XBOOLE_1

:: Boolean Properties of Sets - Theorems
::  by Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 registrations XBOOLE_0;
 requirements BOOLE;
 definitions TARSKI, XBOOLE_0;
 equalities XBOOLE_0;
 expansions TARSKI, XBOOLE_0;
 theorems TARSKI, XBOOLE_0;

begin

reserve x,A,B,X,X9,Y,Y9,Z,V for set;

::$N Modus Barbara
::$L https://en.wikipedia.org/wiki/Syllogism#Modus_Barbara Modus Barbara
theorem
  X c= Y & Y c= Z implies X c= Z;

theorem
  {} c= X;

theorem Th3:
  X c= {} implies X = {}
proof
  assume X c= {};
  hence X c= {} & {} c= X;
end;

theorem Th4:
  (X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
  thus (X \/ Y) \/ Z c= X \/ (Y \/ Z)
  proof
    let x be object;
    assume x in (X \/ Y) \/ Z;
    then x in X \/ Y or x in Z by XBOOLE_0:def 3;
    then x in X or x in Y or x in Z by XBOOLE_0:def 3;
    then x in X or x in Y \/ Z by XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in X \/ (Y \/ Z);
  then x in X or x in Y \/ Z by XBOOLE_0:def 3;
  then x in X or x in Y or x in Z by XBOOLE_0:def 3;
  then x in X \/ Y or x in Z by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proof
  (X \/ Y) \/ Z = X \/ ((Z \/ Z) \/ Y) by Th4
    .= X \/ (Z \/ (Z \/ Y)) by Th4
    .= (X \/ Z) \/ (Y \/ Z) by Th4;
  hence thesis;
end;

theorem
  X \/ (X \/ Y) = X \/ Y
proof
  X \/ (X \/ Y) = (X \/ X) \/ Y by Th4
    .= X \/ Y;
  hence thesis;
end;

theorem Th7:
  X c= X \/ Y
by XBOOLE_0:def 3;

theorem Th8:
  X c= Z & Y c= Z implies X \/ Y c= Z
proof
  assume
A1: X c= Z & Y c= Z;
  let x be object;
  assume x in X \/ Y;
  then x in X or x in Y by XBOOLE_0:def 3;
  hence thesis by A1;
end;

theorem
  X c= Y implies X \/ Z c= Y \/ Z
proof
  assume
A1: X c= Y;
  let x be object;
  assume x in X \/ Z;
  then x in X or x in Z by XBOOLE_0:def 3;
  then x in Y or x in Z by A1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  X c= Y implies X c= Z \/ Y
proof
  Y c= Z \/ Y by Th7;
  hence thesis;
end;

theorem
  X \/ Y c= Z implies X c= Z
proof
  X c= X \/ Y by Th7;
  hence thesis;
end;

theorem Th12:
  X c= Y implies X \/ Y = Y
proof
  assume
A1: X c= Y;
  thus X \/ Y c= Y
  proof
    let x be object;
    assume x in X \/ Y;
    then x in X or x in Y by XBOOLE_0:def 3;
    hence thesis by A1;
  end;
  let x be object;
  thus thesis by XBOOLE_0:def 3;
end;

theorem
  X c= Y & Z c= V implies X \/ Z c= Y \/ V
proof
  assume
A1: X c= Y;
  assume
A2: Z c= V;
  let x be object;
  assume x in X \/ Z;
  then x in X or x in Z by XBOOLE_0:def 3;
  then x in Y or x in V by A1,A2;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  (Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = Y \/ Z
proof
  assume that
A1: Y c= X & Z c= X and
A2: Y c= V & Z c= V implies X c= V;
  Y c= Y \/ Z & Z c= Y \/ Z by Th7;
  hence X c= Y \/ Z by A2;
  thus thesis by A1,Th8;
end;

theorem
  X \/ Y = {} implies X = {};

theorem Th16:
  (X /\ Y) /\ Z = X /\ (Y /\ Z)
proof
  thus (X /\ Y) /\ Z c= X /\ (Y /\ Z)
  proof
    let x be object;
    assume
A1: x in (X /\ Y) /\ Z;
    then
A2: x in Z by XBOOLE_0:def 4;
A3: x in X /\ Y by A1,XBOOLE_0:def 4;
    then
A4: x in X by XBOOLE_0:def 4;
    x in Y by A3,XBOOLE_0:def 4;
    then x in Y /\ Z by A2,XBOOLE_0:def 4;
    hence thesis by A4,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A5: x in X /\ (Y /\ Z);
  then
A6: x in Y /\ Z by XBOOLE_0:def 4;
  then
A7: x in Y by XBOOLE_0:def 4;
A8: x in Z by A6,XBOOLE_0:def 4;
  x in X by A5,XBOOLE_0:def 4;
  then x in X /\ Y by A7,XBOOLE_0:def 4;
  hence thesis by A8,XBOOLE_0:def 4;
end;

theorem Th17:
  X /\ Y c= X
by XBOOLE_0:def 4;

theorem
  X c= Y /\ Z implies X c= Y
proof
  Y /\ Z c= Y by Th17;
  hence thesis;
end;

theorem Th19:
  Z c= X & Z c= Y implies Z c= X /\ Y
proof
  assume
A1: Z c= X & Z c= Y;
  let x be object;
  assume x in Z;
  then x in X & x in Y by A1;
  hence thesis by XBOOLE_0:def 4;
end;

theorem
  (X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = Y /\ Z
proof
  assume that
A1: X c= Y & X c= Z and
A2: V c= Y & V c= Z implies V c= X;
  thus X c= Y /\ Z by A1,Th19;
  Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X by A2;
  hence thesis by Th17;
end;

theorem
  X /\ (X \/ Y) = X
proof
  thus X /\ (X \/ Y) c= X
  by XBOOLE_0:def 4;
  let x be object;
  assume
A1: x in X;
  then x in X \/ Y by XBOOLE_0:def 3;
  hence thesis by A1,XBOOLE_0:def 4;
end;

theorem Th22:
  X \/ (X /\ Y) = X
proof
  thus X \/ (X /\ Y) c= X
  proof
    let x be object;
    assume x in X \/ (X /\ Y);
    then x in X or x in X /\ Y by XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 4;
  end;
  let x be object;
  thus thesis by XBOOLE_0:def 3;
end;

theorem Th23:
  X /\ (Y \/ Z) = X /\ Y \/ X /\ Z
proof
  thus X /\ (Y \/ Z) c= X /\ Y \/ X /\ Z
  proof
    let x be object;
    assume
A1: x in X /\ (Y \/ Z);
    then x in Y \/ Z by XBOOLE_0:def 4;
    then
A2: x in Y or x in Z by XBOOLE_0:def 3;
    x in X by A1,XBOOLE_0:def 4;
    then x in X /\ Y or x in X /\ Z by A2,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in X /\ Y \/ X /\ Z;
  then x in X /\ Y or x in X /\ Z by XBOOLE_0:def 3;
  then
A3: x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;
  then x in Y \/ Z by XBOOLE_0:def 3;
  hence thesis by A3,XBOOLE_0:def 4;
end;

theorem Th24:
  X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z)
proof
  thus X \/ Y /\ Z c= (X \/ Y) /\ (X \/ Z)
  proof
    let x be object;
    assume x in X \/ Y /\ Z;
    then x in X or x in Y /\ Z by XBOOLE_0:def 3;
    then x in X or x in Y & x in Z by XBOOLE_0:def 4;
    then x in X \/ Y & x in X \/ Z by XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A1: x in (X \/ Y) /\ (X \/ Z);
  then x in X \/ Z by XBOOLE_0:def 4;
  then
A2: x in X or x in Z by XBOOLE_0:def 3;
  x in X \/ Y by A1,XBOOLE_0:def 4;
  then x in X or x in Y by XBOOLE_0:def 3;
  then x in X or x in Y /\ Z by A2,XBOOLE_0:def 4;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X)
proof
  thus X /\ Y \/ Y /\ Z \/ Z /\ X = (X /\ Y \/ Y /\ Z \/ Z) /\ (X /\ Y \/ Y /\
  Z \/ X) by Th24
    .= (X /\ Y \/ (Y /\ Z \/ Z)) /\ (X /\ Y \/ Y /\ Z \/ X) by Th4
    .= (X /\ Y \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by Th22
    .= (X /\ Y \/ Z) /\ (X /\ Y \/ X \/ Y /\ Z) by Th4
    .= (X /\ Y \/ Z) /\ (X \/ Y /\ Z) by Th22
    .= (X \/ Z) /\ (Y \/ Z) /\ (X \/ Y /\ Z) by Th24
    .= (X \/ Z) /\ (Y \/ Z) /\ ((X \/ Y) /\ (X \/ Z)) by Th24
    .= (X \/ Y) /\ ((Y \/ Z) /\ (X \/ Z) /\ (X \/ Z)) by Th16
    .= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th16
    .= (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X) by Th16;
end;

theorem Th26:
  X c= Y implies X /\ Z c= Y /\ Z
proof
  assume
A1: X c= Y;
  let x be object;
  assume
A2: x in X /\ Z;
  then x in X by XBOOLE_0:def 4;
  then
A3: x in Y by A1;
  x in Z by A2,XBOOLE_0:def 4;
  hence thesis by A3,XBOOLE_0:def 4;
end;

theorem
  X c= Y & Z c= V implies X /\ Z c= Y /\ V
proof
  assume that
A1: X c= Y and
A2: Z c= V;
  let x be object;
  assume
A3: x in X /\ Z;
  then x in Z by XBOOLE_0:def 4;
  then
A4: x in V by A2;
  x in X by A3,XBOOLE_0:def 4;
  then x in Y by A1;
  hence thesis by A4,XBOOLE_0:def 4;
end;

theorem Th28:
  X c= Y implies X /\ Y = X
proof
  assume
A1: X c= Y;
  thus X /\ Y c= X by Th17;
  let x be object;
  assume
A2: x in X;
  then x in Y by A1;
  hence thesis by A2,XBOOLE_0:def 4;
end;

theorem
  X /\ Y c= X \/ Z
proof
  X /\ Y c= X & X c= X \/ Z by Th7,Th17;
  hence thesis;
end;

theorem
  X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z
proof
  assume
A1: X c= Z;
  thus X \/ Y /\ Z c= (X \/ Y) /\ Z
  proof
    let x be object;
    assume x in X \/ Y /\ Z;
    then
A2: x in X or x in Y /\ Z by XBOOLE_0:def 3;
    then x in X or x in Y & x in Z by XBOOLE_0:def 4;
    then
A3: x in (X \/ Y) by XBOOLE_0:def 3;
    x in Z by A1,A2,XBOOLE_0:def 4;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A4: x in (X \/ Y) /\ Z;
  then x in X \/ Y by XBOOLE_0:def 4;
  then
A5: x in X or x in Y by XBOOLE_0:def 3;
  x in Z by A4,XBOOLE_0:def 4;
  then x in X & x in Z or x in Y /\ Z by A5,XBOOLE_0:def 4;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  (X /\ Y) \/ (X /\ Z) c= Y \/ Z
proof
  now
    let x be object;
    assume x in (X /\ Y) \/ (X /\ Z);
    then x in (X /\ Y) or x in (X /\ Z) by XBOOLE_0:def 3;
    then x in X & x in Y or x in X & x in Z by XBOOLE_0:def 4;
    hence x in Y \/ Z by XBOOLE_0:def 3;
  end;
  hence thesis;
end;

Lm1: X \ Y = {} iff X c= Y
proof
  thus X \ Y = {} implies X c= Y
  by XBOOLE_0:def 5;
  assume
A1: X c= Y;
  now
    let x be object;
    x in X & not x in Y iff contradiction by A1;
    hence x in X \ Y iff x in {} by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  X \ Y = Y \ X implies X = Y
proof
  assume
A1: X \ Y = Y \ X;
  now
    let x be object;
    x in X & not x in Y iff x in Y \ X by A1,XBOOLE_0:def 5;
    hence x in X iff x in Y by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th33:
  X c= Y implies X \ Z c= Y \ Z
proof
  assume
A1: X c= Y;
  let x be object;
  assume
A2: x in X \ Z;
  then x in X by XBOOLE_0:def 5;
  then
A3: x in Y by A1;
  not x in Z by A2,XBOOLE_0:def 5;
  hence thesis by A3,XBOOLE_0:def 5;
end;

theorem Th34:
  X c= Y implies Z \ Y c= Z \ X
proof
  assume
A1: X c= Y;
  let x be object;
  assume
A2: x in Z \ Y;
  then not x in Y by XBOOLE_0:def 5;
  then
A3: not x in X by A1;
  x in Z by A2,XBOOLE_0:def 5;
  hence thesis by A3,XBOOLE_0:def 5;
end;

Lm2: X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof
  thus X \ (Y /\ Z) c= (X \ Y) \/ (X \ Z)
  proof
    let x be object;
    assume
A1: x in X \ (Y /\ Z);
    then not x in (Y /\ Z) by XBOOLE_0:def 5;
    then
A2: not x in Y or not x in Z by XBOOLE_0:def 4;
    x in X by A1,XBOOLE_0:def 5;
    then x in (X \ Y) or x in (X \ Z) by A2,XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
  (X \ Y) c= X \ (Y /\ Z) & X \ Z c= X \ (Y /\ Z) by Th17,Th34;
  hence thesis by Th8;
end;

theorem
  X c= Y & Z c= V implies X \ V c= Y \ Z
proof
  assume X c= Y & Z c= V;
  then X \ V c= Y \ V & Y \ V c= Y \ Z by Th33,Th34;
  hence thesis;
end;

theorem Th36:
  X \ Y c= X
by XBOOLE_0:def 5;

theorem
  X \ Y = {} iff X c= Y by Lm1;

theorem
  X c= Y \ X implies X = {}
proof
  assume
A1: X c= Y \ X;
  thus X c= {}
  proof
    let x be object;
    assume
A2: x in X;
    then x in Y \ X by A1;
    hence thesis by A2,XBOOLE_0:def 5;
  end;
  thus thesis;
end;

theorem Th39:
  X \/ (Y \ X) = X \/ Y
proof
  thus X \/ (Y \ X) c= X \/ Y
  proof
    let x be object;
    assume x in X \/ (Y \ X);
    then x in X or x in Y \ X by XBOOLE_0:def 3;
    then x in X or x in Y by XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in X \/ Y;
  then x in X or x in Y & not x in X by XBOOLE_0:def 3;
  then x in X or x in Y \ X by XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  (X \/ Y) \ Y = X \ Y
proof
  thus for x being object holds x in (X \/ Y) \ Y implies x in X \ Y
  proof let x be object;
    assume
A1: x in (X \/ Y) \ Y;
    then x in (X \/ Y) by XBOOLE_0:def 5;
    then
A2: x in X or x in Y by XBOOLE_0:def 3;
    not x in Y by A1,XBOOLE_0:def 5;
    hence thesis by A2,XBOOLE_0:def 5;
  end;
  thus for x being object holds x in X \ Y implies x in (X \/ Y) \ Y
  proof let x be object;
    assume
A3: x in X \ Y;
    then x in X or x in Y by XBOOLE_0:def 5;
    then
A4: x in (X \/ Y) by XBOOLE_0:def 3;
    not x in Y by A3,XBOOLE_0:def 5;
    hence thesis by A4,XBOOLE_0:def 5;
  end;
end;

theorem Th41:
  (X \ Y) \ Z = X \ (Y \/ Z)
proof
  thus for x being object holds x in (X \ Y) \ Z implies x in X \ (Y \/ Z)
  proof let x be object;
    assume
A1: x in (X \ Y) \ Z;
    then
A2: not x in Z by XBOOLE_0:def 5;
A3: x in (X \ Y) by A1,XBOOLE_0:def 5;
    then
A4: x in X by XBOOLE_0:def 5;
    not x in Y by A3,XBOOLE_0:def 5;
    then not x in (Y \/ Z) by A2,XBOOLE_0:def 3;
    hence thesis by A4,XBOOLE_0:def 5;
  end;
  thus for x being object holds x in X \ (Y \/ Z) implies x in (X \ Y) \ Z
  proof let x be object;
    assume
A5: x in X \ (Y \/ Z);
    then
A6: not x in (Y \/ Z) by XBOOLE_0:def 5;
    then
A7: not x in Y by XBOOLE_0:def 3;
A8: not x in Z by A6,XBOOLE_0:def 3;
    x in X by A5,XBOOLE_0:def 5;
    then x in (X \ Y) by A7,XBOOLE_0:def 5;
    hence thesis by A8,XBOOLE_0:def 5;
  end;
end;

theorem Th42:
  (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proof
  thus (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z)
  proof
    let x be object;
    assume
A1: x in (X \/ Y) \ Z;
    then x in (X \/ Y) by XBOOLE_0:def 5;
    then x in X & not x in Z or x in Y & not x in Z by A1,XBOOLE_0:def 3,def 5;
    then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in (( X \ Z) \/ (Y \ Z));
  then x in (X \ Z) or x in (Y \ Z) by XBOOLE_0:def 3;
  then
A2: x in X & not x in Z or x in Y & not x in Z by XBOOLE_0:def 5;
  then x in (X \/ Y) by XBOOLE_0:def 3;
  hence thesis by A2,XBOOLE_0:def 5;
end;

theorem
  X c= Y \/ Z implies X \ Y c= Z
proof
  assume
A1: X c= Y \/ Z;
  let x be object;
  assume
A2: x in X \ Y;
  then x in X by XBOOLE_0:def 5;
  then
A3: x in Y \/ Z by A1;
  not x in Y by A2,XBOOLE_0:def 5;
  hence thesis by A3,XBOOLE_0:def 3;
end;

theorem
  X \ Y c= Z implies X c= Y \/ Z
proof
  assume
A1: for x being object holds x in X \ Y implies x in Z;
  let x be object;
  assume x in X;
  then x in X \ Y or x in Y by XBOOLE_0:def 5;
  then x in Z or x in Y by A1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  X c= Y implies Y = X \/ (Y \ X)
proof
  assume
A1: X c= Y;
  now
    let x be object;
    x in Y iff x in X or x in (Y \ X) by A1,XBOOLE_0:def 5;
    hence x in Y iff x in X \/ (Y \ X) by XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  X \ (X \/ Y) = {} by Th7,Lm1;

theorem Th47:
  X \ X /\ Y = X \ Y
proof
  now
    let x be object;
    x in X & not x in X /\ Y iff x in X & not x in Y by XBOOLE_0:def 4;
    hence x in X \ X /\ Y iff x in X \ Y by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  X \ (X \ Y) = X /\ Y
proof
  thus for x being object holds x in X \ (X \ Y) implies x in X /\ Y
  proof let x be object;
    assume
A1: x in X \ (X \ Y);
    then not x in (X \ Y) by XBOOLE_0:def 5;
    then
A2: not x in X or x in Y by XBOOLE_0:def 5;
    x in X by A1,XBOOLE_0:def 5;
    hence thesis by A2,XBOOLE_0:def 4;
  end;
  thus for x being object holds x in X /\ Y implies x in X \ (X \ Y)
  proof let x be object;
    assume
A3: x in X /\ Y;
    then not x in X or x in Y by XBOOLE_0:def 4;
    then
A4: not x in (X \ Y) by XBOOLE_0:def 5;
    x in X by A3,XBOOLE_0:def 4;
    hence thesis by A4,XBOOLE_0:def 5;
  end;
end;

theorem Th49:
  X /\ (Y \ Z) = (X /\ Y) \ Z
proof
  now
    let x be object;
    x in X & x in Y & not x in Z iff x in X & x in Y & not x in Z;
    then x in X & x in (Y \ Z) iff x in (X /\ Y) & not x in Z by XBOOLE_0:def 4
,def 5;
    hence x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z by XBOOLE_0:def 4,def 5;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th50:
  X /\ (Y \ Z) = X /\ Y \ X /\ Z
proof
A1: X /\ Y c= X by Th17;
  X /\ Y \ X /\ Z = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Lm2
    .= {} \/ ((X /\ Y) \ Z) by A1,Lm1
    .= (X /\ Y) \ Z;
  hence thesis by Th49;
end;

theorem Th51:
  X /\ Y \/ (X \ Y) = X
proof
  thus X /\ Y \/ (X \ Y) c= X
  proof
    let x be object;
    assume x in X /\ Y \/ (X \ Y);
    then x in X /\ Y or x in (X \ Y) by XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 4,def 5;
  end;
  let x be object;
  assume x in X;
  then x in X & x in Y or x in (X\Y) by XBOOLE_0:def 5;
  then x in X /\ Y or x in (X \ Y) by XBOOLE_0:def 4;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th52:
  X \ (Y \ Z) = (X \ Y) \/ X /\ Z
proof
  thus for x being object
    holds x in X \ (Y \ Z) implies x in (X \ Y) \/ X /\ Z
  proof let x be object;
    assume
A1: x in X \ (Y \ Z);
    then not x in (Y \ Z) by XBOOLE_0:def 5;
    then x in X & not x in Y or x in X & x in Z by A1,XBOOLE_0:def 5;
    then x in (X \ Y) or x in X /\ Z by XBOOLE_0:def 4,def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
    assume x in (X \ Y) \/ X /\ Z;
    then x in (X \ Y) or x in X /\ Z by XBOOLE_0:def 3;
    then
A2: x in X & not x in Y or x in X & x in Z by XBOOLE_0:def 4,def 5;
    then not x in (Y \ Z) by XBOOLE_0:def 5;
    hence thesis by A2,XBOOLE_0:def 5;
end;

theorem
  X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proof
  X \(Y \/ Z) c= X \ Y & X \ (Y \/ Z) c= X \ Z by Th7,Th34;
  hence X \ (Y \/ Z) c= (X \ Y) /\ (X \ Z) by Th19;
  let x be object;
  assume
A1: x in (X \ Y) /\ (X \ Z);
  then
A2: x in (X \ Y) by XBOOLE_0:def 4;
  then
A3: x in X by XBOOLE_0:def 5;
  x in (X \ Z) by A1,XBOOLE_0:def 4;
  then
A4: not x in Z by XBOOLE_0:def 5;
  not x in Y by A2,XBOOLE_0:def 5;
  then not x in (Y \/ Z) by A4,XBOOLE_0:def 3;
  hence thesis by A3,XBOOLE_0:def 5;
end;

theorem
  X \ (Y /\ Z) = (X \ Y) \/ (X \ Z) by Lm2;

theorem Th55:
  (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proof
 for x being object holds
    x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X)
  proof let x be object;
    thus x in (X \/ Y) \ (X /\ Y) implies x in (X \ Y) \/ (Y \ X)
    proof
      assume
A1:   x in (X \/ Y) \ (X /\ Y);
      then not x in (X /\ Y) by XBOOLE_0:def 5;
      then
A2:   not x in X or not x in Y by XBOOLE_0:def 4;
      x in (X \/ Y) by A1,XBOOLE_0:def 5;
      then x in X or x in Y by XBOOLE_0:def 3;
      then x in (X \ Y) or x in( Y \ X) by A2,XBOOLE_0:def 5;
      hence thesis by XBOOLE_0:def 3;
    end;
    assume x in (X \ Y) \/ (Y \ X);
    then x in (X \ Y) or x in (Y \ X) by XBOOLE_0:def 3;
    then x in X & not x in Y or x in Y & not x in X by XBOOLE_0:def 5;
    then ( not x in (X /\ Y))& x in (X \/ Y) by XBOOLE_0:def 3,def 4;
    hence thesis by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

Lm3: X c= Y & Y c< Z implies X c< Z
proof
  assume that
A1: X c= Y and
A2: Y c< Z;
  Y c= Z by A2;
  hence X c= Z & X <> Z by A1,A2,XBOOLE_0:def 10;
end;

theorem
  X c< Y & Y c< Z implies X c< Z
by Lm3;

theorem
  not (X c< Y & Y c< X);

theorem
  X c< Y & Y c= Z implies X c< Z
proof
  assume that
A1: X c< Y and
A2: Y c= Z;
  X c= Y by A1;
  hence X c= Z & X <> Z by A1,A2,XBOOLE_0:def 10;
end;

theorem
  X c= Y & Y c< Z implies X c< Z by Lm3;

theorem Th60:
  X c= Y implies not Y c< X
proof
  assume X c= Y & Y c= X & X <> Y;
  hence contradiction;
end;

theorem
  X <> {} implies {} c< X
proof
  assume
A1: X <> {};
  thus {} c= X;
  thus thesis by A1;
end;

theorem
  not X c< {} by Th3;

::$N Modus Celarent
::$N Modus Darii
::$L https://en.wikipedia.org/wiki/Syllogism#Modus_Celarent Modus Celarent
theorem Th63:
  X c= Y & Y misses Z implies X misses Z by Th3,Th26;

theorem
  A c= X & B c= Y & X misses Y implies A misses B
proof
  assume that
A1: A c= X and
A2: B c= Y and
A3: X misses Y;
  A misses Y by A1,A3,Th63;
  hence thesis by A2,Th63;
end;

theorem
  X misses {};

theorem
  X meets X iff X <> {};

theorem
  X c= Y & X c= Z & Y misses Z implies X = {}
by Th3,Th19;

::$N Modus Darapti
theorem Th68:
  for A being non empty set st A c= Y & A c= Z holds Y meets Z
proof
  let A be non empty set;
  consider x being object such that
A1: x in A by XBOOLE_0:def 1;
  assume A c= Y & A c= Z;
  then x in Y & x in Z by A1;
  hence thesis by XBOOLE_0:3;
end;

theorem
  for A being non empty set st A c= Y holds A meets Y by Th68;

theorem Th70:
  X meets Y \/ Z iff X meets Y or X meets Z
proof
  thus X meets Y \/ Z implies X meets Y or X meets Z
  proof
    assume X meets Y \/ Z;
    then consider x being object such that
A1: x in X & x in Y \/ Z by XBOOLE_0:3;
    x in X & x in Y or x in X & x in Z by A1,XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:3;
  end;
A2: X meets Z implies X meets Y \/ Z
  proof
    assume X meets Z;
    then consider x being object such that
A3: x in X and
A4: x in Z by XBOOLE_0:3;
    x in Y \/ Z by A4,XBOOLE_0:def 3;
    hence thesis by A3,XBOOLE_0:3;
  end;
  X meets Y implies X meets Y \/ Z
  proof
    assume X meets Y;
    then consider x being object such that
A5: x in X and
A6: x in Y by XBOOLE_0:3;
    x in Y \/ Z by A6,XBOOLE_0:def 3;
    hence thesis by A5,XBOOLE_0:3;
  end;
  hence thesis by A2;
end;

theorem
  X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z
proof
  assume that
A1: X \/ Y = Z \/ Y and
A2: X /\ Y = {} and
A3: Z /\ Y = {};
  thus X c= Z
  proof
    let x be object such that
A4: x in X;
    X c= Z \/ Y by A1,Th7;
    then
A5: x in Z \/ Y by A4;
    not x in Y by A2,A4,XBOOLE_0:def 4;
    hence thesis by A5,XBOOLE_0:def 3;
  end;
  let x be object such that
A6: x in Z;
  Z c= X \/ Y by A1,Th7;
  then
A7: x in X \/ Y by A6;
  not x in Y by A3,A6,XBOOLE_0:def 4;
  hence thesis by A7,XBOOLE_0:def 3;
end;

theorem
  X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9
proof
  assume
A1: X9 \/ Y9 = X \/ Y;
  assume X misses X9 & Y misses Y9;
  then
A2: X /\ X9 = {} & Y /\ Y9 = {};
  thus X = X /\ (X9 \/ Y9) by A1,Th7,Th28
    .= X /\ X9 \/ X /\ Y9 by Th23
    .= (X \/ Y) /\ Y9 by A2,Th23
    .= Y9 by A1,Th7,Th28;
end;

theorem
  X c= Y \/ Z & X misses Z implies X c= Y
proof
  assume that
A1: X c= Y \/ Z and
A2: X /\ Z = {};
  X /\ (Y \/ Z)= X by A1,Th28;
  then Y /\ X \/ {} = X by A2,Th23;
  hence thesis by Th17;
end;

theorem Th74:
  X meets Y /\ Z implies X meets Y
proof
  assume X meets Y /\ Z;
  then consider x being object such that
A1: x in X and
A2: x in Y /\ Z by XBOOLE_0:3;
  x in Y by A2,XBOOLE_0:def 4;
  hence thesis by A1,XBOOLE_0:3;
end;

theorem
  X meets Y implies X /\ Y meets Y
proof
  assume X meets Y;
  then consider x being object such that
A1: x in X and
A2: x in Y by XBOOLE_0:3;
  x in X /\ Y by A1,A2,XBOOLE_0:def 4;
  hence thesis by A2,XBOOLE_0:3;
end;

theorem
  Y misses Z implies X /\ Y misses X /\ Z
proof
  assume Y misses Z;
  then (X /\ Z) misses Y by Th74;
  hence thesis by Th74;
end;

theorem
  X meets Y & X c= Z implies X meets Y /\ Z
proof
  assume that
A1: X meets Y and
A2: X c= Z;
  now
    assume
A3: X /\ (Y /\ Z) = {};
    X /\ Y = (X /\ Z) /\ Y by A2,Th28
      .= {} by A3,Th16;
    hence contradiction by A1;
  end;
  hence thesis;
end;

theorem
  X misses Y implies X /\ (Y \/ Z) = X /\ Z
proof
  assume X misses Y;
  then X /\ Y = {};
  hence X /\ (Y \/ Z) = {} \/ X /\ Z by Th23
    .= X /\ Z;
end;

theorem Th79:
  X \ Y misses Y
proof
  not ex x being object st x in (X \ Y) /\ Y
  proof
    given x being object such that
A1: x in (X \ Y) /\ Y;
    x in X \ Y & x in Y by A1,XBOOLE_0:def 4;
    hence contradiction by XBOOLE_0:def 5;
  end;
  hence (X \ Y) /\ Y = {} by XBOOLE_0:def 1;
end;

theorem
  X misses Y implies X misses Y \ Z
proof
  assume
A1: X misses Y;
  assume X meets Y \ Z;
  then consider x being object such that
A2: x in X and
A3: x in Y \ Z by XBOOLE_0:3;
  x in Y by A3,XBOOLE_0:def 5;
  hence thesis by A1,A2,XBOOLE_0:3;
end;

theorem
  X misses Y \ Z implies Y misses X \ Z
proof
  X /\ (Y \ Z) = Y /\ X \ Z by Th49
    .= Y /\ (X \ Z) by Th49;
  hence thesis;
end;

theorem
  X \ Y misses Y \ X
proof
  assume X \ Y meets Y \ X;
  then consider x being object such that
A1: x in X \ Y and
A2: x in Y \ X by XBOOLE_0:3;
  x in X by A1,XBOOLE_0:def 5;
  hence thesis by A2,XBOOLE_0:def 5;
end;

theorem Th83:
  X misses Y iff X \ Y = X
proof
  thus X misses Y implies X \ Y = X
  proof
    assume
A1: X /\ Y = {};
    thus for x being object holds x in X \ Y implies x in X by XBOOLE_0:def 5;
    let x be object;
    not x in X /\ Y implies not x in X or not x in Y by XBOOLE_0:def 4;
    hence thesis by A1,XBOOLE_0:def 5;
  end;
  assume
A2: X \ Y = X;
  not ex x being object st x in X /\ Y
  proof
    given x being object such that
A3: x in X /\ Y;
    x in X & x in Y by A3,XBOOLE_0:def 4;
    hence contradiction by A2,XBOOLE_0:def 5;
  end;
  hence thesis by XBOOLE_0:4;
end;

theorem
  X meets Y & X misses Z implies X meets Y \ Z
proof
  assume that
A1: X meets Y and
A2: X misses Z;
  X /\ (Y \ Z) = X /\ Y \ X /\ Z by Th50
    .= X /\ Y \ {} by A2;
  hence X /\ (Y \ Z) <> {} by A1;
end;

theorem
  X c= Y implies X misses Z \ Y
proof
  assume
A1: X c= Y;
  thus X /\ (Z \ Y) = Z /\ X \ Y by Th49
    .= Z /\ (X \ Y) by Th49
    .= Z /\ {} by A1,Lm1
    .= {};
end;

theorem Th86:
  X c= Y & X misses Z implies X c= Y \ Z
proof
  assume
A1: X c= Y & X /\ Z = {};
  let x be object;
  assume x in X;
  then x in Y & not x in Z by A1,XBOOLE_0:def 4;
  hence thesis by XBOOLE_0:def 5;
end;

theorem
  Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y
proof
  assume
A1: Y misses Z;
  thus (X \/ Z) \ Y = (X \ Y) \/ (Z \ Y) by Th42
    .= (X \ Y) \/ Z by A1,Th83;
end;

theorem Th88:
  X misses Y implies (X \/ Y) \ Y = X
proof
  assume
A1: X misses Y;
  thus (X \/ Y) \ Y = (X \ Y) \/ (Y \ Y) by Th42
    .= (X \ Y) \/ {} by Lm1
    .= X by A1,Th83;
end;

theorem Th89:
  X /\ Y misses X \ Y
proof
  now
    let x be object;
    not (x in X & x in Y & not x in Y);
    hence not (x in X /\ Y & x in X \ Y) by XBOOLE_0:def 4,def 5;
  end;
  hence thesis by XBOOLE_0:3;
end;

theorem
  X \ (X /\ Y) misses Y
proof
  X \ (X /\ Y) = X \ Y by Th47;
  hence thesis by Th79;
end;

theorem
  (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
  set S1 = X \ (Y \/ Z), S2 = Y \ (X \/ Z), S3 = Z \ (X \/ Y), S4 = X /\ Y /\
  Z;
  thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/
  (Y \ X))) by Th42
    .= (S1 \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
    .= (S1 \/ S2) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
    .= (S1 \/ S2) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th55
    .= (S1 \/ S2) \/ (S4 \/ S3) by Th52
    .= (S1 \/ S2 \/ S4) \/ S3 by Th4
    .= (S1 \/ S4 \/ S2) \/ S3 by Th4
    .= (S1 \/ S4) \/ (S2 \/ S3) by Th4
    .= (S1 \/ X /\ (Y /\ Z)) \/ (S2 \/ S3) by Th16
    .= X \ ((Y \/ Z) \ (Y /\ Z)) \/ (S2 \/ S3) by Th52
    .= X \ ((Y \ Z) \/ (Z \ Y)) \/ (S2 \/ (Z \ (Y \/ X))) by Th55
    .= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ (Z \/ X)) \/ (Z \ Y \ X)) by Th41
    .= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ Z \ X) \/ (Z \ Y \ X)) by Th41
    .= X \+\ (Y \+\ Z) by Th42;
end;

theorem
  X \+\ X = {} by Lm1;

theorem Th93:
  X \/ Y = (X \+\ Y) \/ X /\ Y
proof
  thus X \/ Y = ((X \ Y) \/ X /\ Y) \/ Y by Th51
    .= (X \ Y) \/ (X /\ Y \/ Y) by Th4
    .= (X \ Y) \/ Y by Th22
    .= (X \ Y) \/ ((Y \ X) \/ (Y /\ X)) by Th51
    .= (X \+\ Y) \/ X /\ Y by Th4;
end;

Lm4: X /\ Y misses X \+\ Y
proof
  X /\ Y misses X \ Y & X /\ Y misses Y \ X by Th89;
  hence thesis by Th70;
end;

Lm5: X \+\ Y = (X \/ Y) \ X /\ Y
proof
  thus X \+\ Y = (X \ X /\ Y) \/ (Y \ X) by Th47
    .= (X \ X /\ Y) \/ (Y \ X /\ Y) by Th47
    .= (X \/ Y) \ X /\ Y by Th42;
end;

theorem
  X \/ Y = X \+\ Y \+\ X /\ Y
proof
  X /\ Y misses X \+\ Y by Lm4;
  then (X \+\ Y) \ X /\ Y = X \+\ Y & X /\ Y \ (X \+\ Y) = X /\ Y by Th83;
  hence thesis by Th93;
end;

theorem
  X /\ Y = X \+\ Y \+\ (X \/ Y)
proof
  X \+\ Y = (X \/ Y) \ X /\ Y by Lm5;
  then X \+\ Y c= X \/ Y by Th36;
  then
A1: (X \+\ Y) \ (X \/ Y) = {} by Lm1;
  X \/ Y = (X \+\ Y) \/ X /\ Y by Th93;
  hence thesis by A1,Lm4,Th88;
end;

theorem
  X \ Y c= X \+\ Y by Th7;

theorem
  X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z by Th8;

theorem
  X \/ Y = X \+\ (Y \ X)
proof
A1: Y \ X \ X = Y \ (X \/ X) by Th41
    .= Y \ X;
  X \ (Y \ X) = (X \ Y) \/ X /\ X by Th52
    .= X by Th12,Th36;
  hence thesis by A1,Th39;
end;

theorem
  (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proof
  thus (X \+\ Y) \ Z = (X \ Y \ Z) \/ (Y \ X \ Z) by Th42
    .= (X \ (Y \/ Z)) \/ (Y \ X \ Z) by Th41
    .= (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)) by Th41;
end;

theorem
  X \ Y = X \+\ (X /\ Y)
proof
  X /\ Y c= X by Th17;
  then X /\ Y \ X = {} by Lm1;
  hence thesis by Th47;
end;

theorem
  X \+\ Y = (X \/ Y) \ X /\ Y by Lm5;

theorem
  X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z
proof
  thus X \ (Y \+\ Z) = X \ ((Y \/ Z) \ Y /\ Z) by Lm5
    .= X \ (Y \/ Z) \/ X /\ (Y /\ Z) by Th52
    .= X \ (Y \/ Z) \/ X /\ Y /\ Z by Th16;
end;

theorem
  X /\ Y misses X \+\ Y by Lm4;

theorem
  X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable;

begin :: Addenda

theorem
  for X, Y being set st X c< Y holds Y \ X <> {} by Th60,Lm1;

theorem Th106:
  X c= A \ B implies X c= A & X misses B
proof
  assume
A1: X c= A \ B;
  A \ B c= A by Th36;
  hence X c= A by A1;
  now
    let x be object;
    assume x in X;
    then x in A \ B by A1;
    hence not x in B by XBOOLE_0:def 5;
  end;
  hence thesis by XBOOLE_0:3;
end;

theorem
  X c= A \+\ B iff X c= A \/ B & X misses A /\ B
proof
  A \+\ B = (A \/ B) \ A /\ B by Lm5;
  hence thesis by Th86,Th106;
end;

theorem
  X c= A implies X /\ Y c= A
proof
  X /\ Y c= X by Th17;
  hence thesis;
end;

theorem Th109:
  X c= A implies X \ Y c= A
proof
  X \ Y c= X by Th36;
  hence thesis;
end;

theorem
  X c= A & Y c= A implies X \+\ Y c= A
proof
  assume X c= A & Y c= A;
  then X \ Y c= A & Y \ X c= A by Th109;
  hence thesis by Th8;
end;

theorem Th111:
  (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
proof
  thus (X /\ Z) \ (Y /\ Z) = ((X /\ Z) \ Y) \/ ((X /\ Z) \ Z) by Lm2
    .= ((X /\ Z) \ Y) \/ (X /\ (Z \ Z)) by Th49
    .= ((X /\ Z) \ Y) \/ (X /\ {}) by Lm1
    .= (X \ Y) /\ Z by Th49;
end;

theorem
  (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
proof
  thus (X /\ Z) \+\ (Y /\ Z) = ((X \ Y) /\ Z) \/ ((Y /\ Z) \ (X /\ Z)) by Th111
    .= ((X \ Y) /\ Z) \/ ((Y \ X) /\ Z) by Th111
    .= (X \+\ Y) /\ Z by Th23;
end;

theorem
  X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V)
proof
  X \/ Y \/ Z \/ V = X \/ Y \/ (Z \/ V) by Th4
    .= X \/ (Y \/ (Z \/ V)) by Th4
    .= X \/ (Y \/ Z \/ V) by Th4;
  hence thesis;
end;

theorem
  for A,B,C,D being set st A misses D & B misses D & C misses D holds
  A \/ B \/ C misses D
proof
  let A,B,C,D be set;
  assume A misses D & B misses D;
  then A \/ B misses D by Th70;
  hence thesis by Th70;
end;

::$CT

theorem
  X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
proof
  thus X /\ (Y /\ Z) = X /\ X /\ Y /\ Z by Th16
    .= X /\ (X /\ Y) /\ Z by Th16
    .= (X /\ Y) /\ (X /\ Z) by Th16;
end;

theorem
  for P,G,C being set st C c= G holds P \ C = (P \ G) \/ (P /\ (G \ C))
proof
  let P,G,C be set;
  assume C c= G;
  then
A1: P \ G c= P \ C by Th34;
  thus P \ C c= (P \ G) \/ (P /\ (G \ C))
  proof
    let x be object;
    assume x in P \ C;
    then x in P & not x in G or x in P & x in G & not x in C by XBOOLE_0:def 5;
    then x in P \ G or x in P & x in G \ C by XBOOLE_0:def 5;
    then x in P \ G or x in P /\ (G \ C) by XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
  P /\ (G \ C) = (P /\ G) \ C & (P /\ G) \ C c= P \ C by Th17,Th33,Th49;
  hence thesis by A1,Th8;
end;