:: XBOOLE_1 semantic presentation

begin


theorem Th1: :: XBOOLE_1:1
for X, Y, Z being set st X c= Y & Y c= Z holds
X c= Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & Y c= Z implies X c= Z )
assume that
A1: X c= Y and
A2: Y c= Z ; ::_thesis: X c= Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume  x in X ; ::_thesis: x in Z
then  x in Y by A1, TARSKI:def_3;
hence  x in Z by A2, TARSKI:def_3; ::_thesis: verum
end;

theorem Th2: :: XBOOLE_1:2
for X being set holds {} c= X
proof
let X be set ; ::_thesis: {} c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} or x in X )
thus  ( not x in {} or x in X ) ; ::_thesis: verum
end;

theorem Th3: :: XBOOLE_1:3
for X being set st X c= {} holds
X = {}
proof
let X be set ; ::_thesis: ( X c= {} implies X = {} )
assume  X c= {} ; ::_thesis: X = {}
hence  ( X c= {} & {} c= X ) by Th2; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th4: :: XBOOLE_1:4
for X, Y, Z being set holds (X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
let X, Y, Z be set ; ::_thesis: (X \/ Y) \/ Z = X \/ (Y \/ Z)
thus  (X \/ Y) \/ Z c= X \/ (Y \/ Z) :: according to XBOOLE_0:def_10 ::_thesis: X \/ (Y \/ Z) c= (X \/ Y) \/ Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) \/ Z or x in X \/ (Y \/ Z) )
assume  x in (X \/ Y) \/ Z ; ::_thesis: 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  x in X \/ (Y \/ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (Y \/ Z) or x in (X \/ Y) \/ Z )
assume  x in X \/ (Y \/ Z) ; ::_thesis: 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  x in (X \/ Y) \/ Z by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:5
for X, Y, Z being set holds (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proof
let X, Y, Z be set ; ::_thesis: (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
(X \/ Y) \/ Z = X \/ ((Z \/ Z) \/ Y) by Th4
.= X \/ (Z \/ (Z \/ Y)) by Th4
.= (X \/ Z) \/ (Y \/ Z) by Th4 ;
hence  (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) ; ::_thesis: verum
end;

theorem :: XBOOLE_1:6
for X, Y being set holds X \/ (X \/ Y) = X \/ Y
proof
let X, Y be set ; ::_thesis: X \/ (X \/ Y) = X \/ Y
X \/ (X \/ Y) = (X \/ X) \/ Y by Th4
.= X \/ Y ;
hence  X \/ (X \/ Y) = X \/ Y ; ::_thesis: verum
end;

theorem Th7: :: XBOOLE_1:7
for X, Y being set holds X c= X \/ Y
proof
let X, Y be set ; ::_thesis: X c= X \/ Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \/ Y )
thus  ( not x in X or x in X \/ Y ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th8: :: XBOOLE_1:8
for X, Z, Y being set st X c= Z & Y c= Z holds
X \/ Y c= Z
proof
let X, Z, Y be set ; ::_thesis: ( X c= Z & Y c= Z implies X \/ Y c= Z )
assume A1: ( X c= Z & Y c= Z ) ; ::_thesis: X \/ Y c= Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Y or x in Z )
assume  x in X \/ Y ; ::_thesis: x in Z
then  ( x in X or x in Y ) by XBOOLE_0:def_3;
hence  x in Z by A1, TARSKI:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:9
for X, Y, Z being set st X c= Y holds
X \/ Z c= Y \/ Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies X \/ Z c= Y \/ Z )
assume A1: X c= Y ; ::_thesis: X \/ Z c= Y \/ Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Z or x in Y \/ Z )
assume  x in X \/ Z ; ::_thesis: x in Y \/ Z
then  ( x in X or x in Z ) by XBOOLE_0:def_3;
then  ( x in Y or x in Z ) by A1, TARSKI:def_3;
hence  x in Y \/ Z by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:10
for X, Y, Z being set st X c= Y holds
X c= Z \/ Y
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies X c= Z \/ Y )
 Y c= Z \/ Y by Th7;
hence  ( X c= Y implies X c= Z \/ Y ) by Th1; ::_thesis: verum
end;

theorem :: XBOOLE_1:11
for X, Y, Z being set st X \/ Y c= Z holds
X c= Z
proof
let X, Y, Z be set ; ::_thesis: ( X \/ Y c= Z implies X c= Z )
 X c= X \/ Y by Th7;
hence  ( X \/ Y c= Z implies X c= Z ) by Th1; ::_thesis: verum
end;

theorem Th12: :: XBOOLE_1:12
for X, Y being set st X c= Y holds
X \/ Y = Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies X \/ Y = Y )
assume A1: X c= Y ; ::_thesis: X \/ Y = Y
thus  X \/ Y c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X \/ Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Y or x in Y )
assume  x in X \/ Y ; ::_thesis: x in Y
then  ( x in X or x in Y ) by XBOOLE_0:def_3;
hence  x in Y by A1, TARSKI:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X \/ Y )
thus  ( not x in Y or x in X \/ Y ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:13
for X, Y, Z, V being set st X c= Y & Z c= V holds
X \/ Z c= Y \/ V
proof
let X, Y, Z, V be set ; ::_thesis: ( X c= Y & Z c= V implies X \/ Z c= Y \/ V )
assume A1: X c= Y ; ::_thesis: ( not Z c= V or X \/ Z c= Y \/ V )
assume A2: Z c= V ; ::_thesis: X \/ Z c= Y \/ V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Z or x in Y \/ V )
assume  x in X \/ Z ; ::_thesis: x in Y \/ V
then  ( x in X or x in Z ) by XBOOLE_0:def_3;
then  ( x in Y or x in V ) by A1, A2, TARSKI:def_3;
hence  x in Y \/ V by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:14
for Y, X, Z being set st Y c= X & Z c= X & ( for V being set st Y c= V & Z c= V holds
X c= V ) holds
X = Y \/ Z
proof
let Y, X, Z be set ; ::_thesis: ( Y c= X & Z c= X & ( for V being set st Y c= V & Z c= V holds
X c= V ) implies X = Y \/ Z )
assume that
A1: ( Y c= X & Z c= X ) and
A2: for V being set st Y c= V & Z c= V holds
X c= V ; ::_thesis: X = Y \/ Z
 ( Y c= Y \/ Z & Z c= Y \/ Z ) by Th7;
hence  X c= Y \/ Z by A2; :: according to XBOOLE_0:def_10 ::_thesis: Y \/ Z c= X
thus  Y \/ Z c= X by A1, Th8; ::_thesis: verum
end;

theorem :: XBOOLE_1:15
for X, Y being set st X \/ Y = {} holds
X = {} ;

theorem Th16: :: XBOOLE_1:16
for X, Y, Z being set holds (X /\ Y) /\ Z = X /\ (Y /\ Z)
proof
let X, Y, Z be set ; ::_thesis: (X /\ Y) /\ Z = X /\ (Y /\ Z)
thus  (X /\ Y) /\ Z c= X /\ (Y /\ Z) :: according to XBOOLE_0:def_10 ::_thesis: X /\ (Y /\ Z) c= (X /\ Y) /\ Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) /\ Z or x in X /\ (Y /\ Z) )
assume A1: x in (X /\ Y) /\ Z ; ::_thesis: 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  x in X /\ (Y /\ Z) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (Y /\ Z) or x in (X /\ Y) /\ Z )
assume A5: x in X /\ (Y /\ Z) ; ::_thesis: 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  x in (X /\ Y) /\ Z by A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th17: :: XBOOLE_1:17
for X, Y being set holds X /\ Y c= X
proof
let X, Y be set ; ::_thesis: X /\ Y c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ Y or x in X )
thus  ( not x in X /\ Y or x in X ) by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: XBOOLE_1:18
for X, Y, Z being set st X c= Y /\ Z holds
X c= Y
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y /\ Z implies X c= Y )
 Y /\ Z c= Y by Th17;
hence  ( X c= Y /\ Z implies X c= Y ) by Th1; ::_thesis: verum
end;

theorem Th19: :: XBOOLE_1:19
for Z, X, Y being set st Z c= X & Z c= Y holds
Z c= X /\ Y
proof
let Z, X, Y be set ; ::_thesis: ( Z c= X & Z c= Y implies Z c= X /\ Y )
assume A1: ( Z c= X & Z c= Y ) ; ::_thesis: Z c= X /\ Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in X /\ Y )
assume  x in Z ; ::_thesis: x in X /\ Y
then  ( x in X & x in Y ) by A1, TARSKI:def_3;
hence  x in X /\ Y by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: XBOOLE_1:20
for X, Y, Z being set st X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds
V c= X ) holds
X = Y /\ Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds
V c= X ) implies X = Y /\ Z )
assume that
A1: ( X c= Y & X c= Z ) and
A2: for V being set st V c= Y & V c= Z holds
V c= X ; ::_thesis: X = Y /\ Z
thus  X c= Y /\ Z by A1, Th19; :: according to XBOOLE_0:def_10 ::_thesis: Y /\ Z c= X
 ( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;
hence  Y /\ Z c= X by Th17; ::_thesis: verum
end;

theorem :: XBOOLE_1:21
for X, Y being set holds X /\ (X \/ Y) = X
proof
let X, Y be set ; ::_thesis: X /\ (X \/ Y) = X
thus  X /\ (X \/ Y) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X /\ (X \/ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (X \/ Y) or x in X )
thus  ( not x in X /\ (X \/ Y) or x in X ) by XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X /\ (X \/ Y) )
assume A1: x in X ; ::_thesis: x in X /\ (X \/ Y)
then  x in X \/ Y by XBOOLE_0:def_3;
hence  x in X /\ (X \/ Y) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th22: :: XBOOLE_1:22
for X, Y being set holds X \/ (X /\ Y) = X
proof
let X, Y be set ; ::_thesis: X \/ (X /\ Y) = X
thus  X \/ (X /\ Y) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X \/ (X /\ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (X /\ Y) or x in X )
assume  x in X \/ (X /\ Y) ; ::_thesis: x in X
then  ( x in X or x in X /\ Y ) by XBOOLE_0:def_3;
hence  x in X by XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \/ (X /\ Y) )
thus  ( not x in X or x in X \/ (X /\ Y) ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th23: :: XBOOLE_1:23
for X, Y, Z being set holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
proof
let X, Y, Z be set ; ::_thesis: X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
thus  X /\ (Y \/ Z) c= (X /\ Y) \/ (X /\ Z) :: according to XBOOLE_0:def_10 ::_thesis: (X /\ Y) \/ (X /\ Z) c= X /\ (Y \/ Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (Y \/ Z) or x in (X /\ Y) \/ (X /\ Z) )
assume A1: x in X /\ (Y \/ Z) ; ::_thesis: x in (X /\ Y) \/ (X /\ 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  x in (X /\ Y) \/ (X /\ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) \/ (X /\ Z) or x in X /\ (Y \/ Z) )
assume  x in (X /\ Y) \/ (X /\ Z) ; ::_thesis: x in X /\ (Y \/ 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  x in X /\ (Y \/ Z) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th24: :: XBOOLE_1:24
for X, Y, Z being set holds X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
proof
let X, Y, Z be set ; ::_thesis: X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
thus  X \/ (Y /\ Z) c= (X \/ Y) /\ (X \/ Z) :: according to XBOOLE_0:def_10 ::_thesis: (X \/ Y) /\ (X \/ Z) c= X \/ (Y /\ Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (Y /\ Z) or x in (X \/ Y) /\ (X \/ Z) )
assume  x in X \/ (Y /\ Z) ; ::_thesis: x in (X \/ Y) /\ (X \/ 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  x in (X \/ Y) /\ (X \/ Z) by XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) /\ (X \/ Z) or x in X \/ (Y /\ Z) )
assume A1: x in (X \/ Y) /\ (X \/ Z) ; ::_thesis: x in X \/ (Y /\ 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  x in X \/ (Y /\ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:25
for X, Y, Z being set holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
proof
let X, Y, Z be set ; ::_thesis: ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
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 ; ::_thesis: verum
end;

theorem Th26: :: XBOOLE_1:26
for X, Y, Z being set st X c= Y holds
X /\ Z c= Y /\ Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies X /\ Z c= Y /\ Z )
assume A1: X c= Y ; ::_thesis: X /\ Z c= Y /\ Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ Z or x in Y /\ Z )
assume A2: x in X /\ Z ; ::_thesis: x in Y /\ Z
then  x in X by XBOOLE_0:def_4;
then A3: x in Y by A1, TARSKI:def_3;
 x in Z by A2, XBOOLE_0:def_4;
hence  x in Y /\ Z by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: XBOOLE_1:27
for X, Y, Z, V being set st X c= Y & Z c= V holds
X /\ Z c= Y /\ V
proof
let X, Y, Z, V be set ; ::_thesis: ( X c= Y & Z c= V implies X /\ Z c= Y /\ V )
assume that
A1: X c= Y and
A2: Z c= V ; ::_thesis: X /\ Z c= Y /\ V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ Z or x in Y /\ V )
assume A3: x in X /\ Z ; ::_thesis: x in Y /\ V
then  x in Z by XBOOLE_0:def_4;
then A4: x in V by A2, TARSKI:def_3;
 x in X by A3, XBOOLE_0:def_4;
then  x in Y by A1, TARSKI:def_3;
hence  x in Y /\ V by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th28: :: XBOOLE_1:28
for X, Y being set st X c= Y holds
X /\ Y = X
proof
let X, Y be set ; ::_thesis: ( X c= Y implies X /\ Y = X )
assume A1: X c= Y ; ::_thesis: X /\ Y = X
thus  X /\ Y c= X by Th17; :: according to XBOOLE_0:def_10 ::_thesis: X c= X /\ Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X /\ Y )
assume A2: x in X ; ::_thesis: x in X /\ Y
then  x in Y by A1, TARSKI:def_3;
hence  x in X /\ Y by A2, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: XBOOLE_1:29
for X, Y, Z being set holds X /\ Y c= X \/ Z
proof
let X, Y, Z be set ; ::_thesis: X /\ Y c= X \/ Z
 ( X /\ Y c= X & X c= X \/ Z ) by Th7, Th17;
hence  X /\ Y c= X \/ Z by Th1; ::_thesis: verum
end;

theorem :: XBOOLE_1:30
for X, Z, Y being set st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
proof
let X, Z, Y be set ; ::_thesis: ( X c= Z implies X \/ (Y /\ Z) = (X \/ Y) /\ Z )
assume A1: X c= Z ; ::_thesis: X \/ (Y /\ Z) = (X \/ Y) /\ Z
thus  X \/ (Y /\ Z) c= (X \/ Y) /\ Z :: according to XBOOLE_0:def_10 ::_thesis: (X \/ Y) /\ Z c= X \/ (Y /\ Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (Y /\ Z) or x in (X \/ Y) /\ Z )
assume  x in X \/ (Y /\ Z) ; ::_thesis: 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, TARSKI:def_3, XBOOLE_0:def_4;
hence  x in (X \/ Y) /\ Z by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) /\ Z or x in X \/ (Y /\ Z) )
assume A4: x in (X \/ Y) /\ Z ; ::_thesis: 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  x in X \/ (Y /\ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:31
for X, Y, Z being set holds (X /\ Y) \/ (X /\ Z) c= Y \/ Z
proof
let X, Y, Z be set ; ::_thesis: (X /\ Y) \/ (X /\ Z) c= Y \/ Z
now__::_thesis:_for_x_being_set_st_x_in_(X_/\_Y)_\/_(X_/\_Z)_holds_
x_in_Y_\/_Z
let x be set ; ::_thesis: ( x in (X /\ Y) \/ (X /\ Z) implies x in Y \/ Z )
assume  x in (X /\ Y) \/ (X /\ Z) ; ::_thesis: x in Y \/ 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; ::_thesis: verum
end;
hence  (X /\ Y) \/ (X /\ Z) c= Y \/ Z by TARSKI:def_3; ::_thesis: verum
end;

Lm1:  for X, Y being set holds
( X \ Y = {} iff X c= Y )
proof
let X, Y be set ; ::_thesis: ( X \ Y = {} iff X c= Y )
thus  ( X \ Y = {} implies X c= Y ) ::_thesis: ( X c= Y implies X \ Y = {} )
proof
assume A1: X \ Y = {} ; ::_thesis: X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume  ( x in X & not x in Y ) ; ::_thesis: contradiction
hence  contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A2: X c= Y ; ::_thesis: X \ Y = {}
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_\_Y_iff_x_in_{}_)
let x be set ; ::_thesis: ( x in X \ Y iff x in {} )
 ( ( x in X & not x in Y ) iff contradiction ) by A2, TARSKI:def_3;
hence  ( x in X \ Y iff x in {} ) by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X \ Y = {} by TARSKI:1; ::_thesis: verum
end;

theorem :: XBOOLE_1:32
for X, Y being set st X \ Y = Y \ X holds
X = Y
proof
let X, Y be set ; ::_thesis: ( X \ Y = Y \ X implies X = Y )
assume A1: X \ Y = Y \ X ; ::_thesis: X = Y
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_iff_x_in_Y_)
let x be set ; ::_thesis: ( x in X iff x in Y )
 ( ( 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; ::_thesis: verum
end;
hence  X = Y by TARSKI:1; ::_thesis: verum
end;

theorem Th33: :: XBOOLE_1:33
for X, Y, Z being set st X c= Y holds
X \ Z c= Y \ Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies X \ Z c= Y \ Z )
assume A1: X c= Y ; ::_thesis: X \ Z c= Y \ Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ Z or x in Y \ Z )
assume A2: x in X \ Z ; ::_thesis: x in Y \ Z
then  x in X by XBOOLE_0:def_5;
then A3: x in Y by A1, TARSKI:def_3;
 not x in Z by A2, XBOOLE_0:def_5;
hence  x in Y \ Z by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th34: :: XBOOLE_1:34
for X, Y, Z being set st X c= Y holds
Z \ Y c= Z \ X
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies Z \ Y c= Z \ X )
assume A1: X c= Y ; ::_thesis: Z \ Y c= Z \ X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z \ Y or x in Z \ X )
assume A2: x in Z \ Y ; ::_thesis: x in Z \ X
then  not x in Y by XBOOLE_0:def_5;
then A3: not x in X by A1, TARSKI:def_3;
 x in Z by A2, XBOOLE_0:def_5;
hence  x in Z \ X by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

Lm2:  for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof
let X, Y, Z be set ; ::_thesis: X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
thus  X \ (Y /\ Z) c= (X \ Y) \/ (X \ Z) :: according to XBOOLE_0:def_10 ::_thesis: (X \ Y) \/ (X \ Z) c= X \ (Y /\ Z)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ (Y /\ Z) or x in (X \ Y) \/ (X \ Z) )
assume A1: x in X \ (Y /\ Z) ; ::_thesis: x in (X \ Y) \/ (X \ 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  x in (X \ Y) \/ (X \ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( X \ Y c= X \ (Y /\ Z) & X \ Z c= X \ (Y /\ Z) ) by Th17, Th34;
hence  (X \ Y) \/ (X \ Z) c= X \ (Y /\ Z) by Th8; ::_thesis: verum
end;

theorem :: XBOOLE_1:35
for X, Y, Z, V being set st X c= Y & Z c= V holds
X \ V c= Y \ Z
proof
let X, Y, Z, V be set ; ::_thesis: ( X c= Y & Z c= V implies X \ V c= Y \ Z )
assume  ( X c= Y & Z c= V ) ; ::_thesis: X \ V c= Y \ Z
then  ( X \ V c= Y \ V & Y \ V c= Y \ Z ) by Th33, Th34;
hence  X \ V c= Y \ Z by Th1; ::_thesis: verum
end;

theorem Th36: :: XBOOLE_1:36
for X, Y being set holds X \ Y c= X
proof
let X, Y be set ; ::_thesis: X \ Y c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ Y or x in X )
thus  ( not x in X \ Y or x in X ) by XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: XBOOLE_1:37
for X, Y being set holds
( X \ Y = {} iff X c= Y ) by Lm1;

theorem :: XBOOLE_1:38
for X, Y being set st X c= Y \ X holds
X = {}
proof
let X, Y be set ; ::_thesis: ( X c= Y \ X implies X = {} )
assume A1: X c= Y \ X ; ::_thesis: X = {}
thus  X c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in {} )
assume A2: x in X ; ::_thesis: x in {}
then  x in Y \ X by A1, TARSKI:def_3;
hence  x in {} by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  {} c= X by Th2; ::_thesis: verum
end;

theorem Th39: :: XBOOLE_1:39
for X, Y being set holds X \/ (Y \ X) = X \/ Y
proof
let X, Y be set ; ::_thesis: X \/ (Y \ X) = X \/ Y
thus  X \/ (Y \ X) c= X \/ Y :: according to XBOOLE_0:def_10 ::_thesis: X \/ Y c= X \/ (Y \ X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (Y \ X) or x in X \/ Y )
assume  x in X \/ (Y \ X) ; ::_thesis: x in X \/ Y
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  x in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Y or x in X \/ (Y \ X) )
assume  x in X \/ Y ; ::_thesis: x in X \/ (Y \ X)
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  x in X \/ (Y \ X) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:40
for X, Y being set holds (X \/ Y) \ Y = X \ Y
proof
let X, Y be set ; ::_thesis: (X \/ Y) \ Y = X \ Y
thus  for x being set st x in (X \/ Y) \ Y holds
x in X \ Y :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X \ Y c= (X \/ Y) \ Y
proof
let x be set ; ::_thesis: ( x in (X \/ Y) \ Y implies x in X \ Y )
assume A1: x in (X \/ Y) \ Y ; ::_thesis: x in X \ 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  x in X \ Y by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  for x being set st x in X \ Y holds
x in (X \/ Y) \ Y :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X \ Y implies x in (X \/ Y) \ Y )
assume A3: x in X \ Y ; ::_thesis: x in (X \/ Y) \ 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  x in (X \/ Y) \ Y by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem Th41: :: XBOOLE_1:41
for X, Y, Z being set holds (X \ Y) \ Z = X \ (Y \/ Z)
proof
let X, Y, Z be set ; ::_thesis: (X \ Y) \ Z = X \ (Y \/ Z)
thus  for x being set st x in (X \ Y) \ Z holds
x in X \ (Y \/ Z) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X \ (Y \/ Z) c= (X \ Y) \ Z
proof
let x be set ; ::_thesis: ( x in (X \ Y) \ Z implies x in X \ (Y \/ Z) )
assume A1: x in (X \ Y) \ Z ; ::_thesis: 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  x in X \ (Y \/ Z) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  for x being set st x in X \ (Y \/ Z) holds
x in (X \ Y) \ Z :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X \ (Y \/ Z) implies x in (X \ Y) \ Z )
assume A5: x in X \ (Y \/ Z) ; ::_thesis: 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  x in (X \ Y) \ Z by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem Th42: :: XBOOLE_1:42
for X, Y, Z being set holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proof
let X, Y, Z be set ; ::_thesis: (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
thus  (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z) :: according to XBOOLE_0:def_10 ::_thesis: (X \ Z) \/ (Y \ Z) c= (X \/ Y) \ Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) \ Z or x in (X \ Z) \/ (Y \ Z) )
assume A1: x in (X \/ Y) \ Z ; ::_thesis: x in (X \ Z) \/ (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, XBOOLE_0:def_5;
then  ( x in X \ Z or x in Y \ Z ) by XBOOLE_0:def_5;
hence  x in (X \ Z) \/ (Y \ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \ Z) \/ (Y \ Z) or x in (X \/ Y) \ Z )
assume  x in (X \ Z) \/ (Y \ Z) ; ::_thesis: x in (X \/ 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  x in (X \/ Y) \ Z by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: XBOOLE_1:43
for X, Y, Z being set st X c= Y \/ Z holds
X \ Y c= Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y \/ Z implies X \ Y c= Z )
assume A1: X c= Y \/ Z ; ::_thesis: X \ Y c= Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ Y or x in Z )
assume A2: x in X \ Y ; ::_thesis: x in Z
then  x in X by XBOOLE_0:def_5;
then A3: x in Y \/ Z by A1, TARSKI:def_3;
 not x in Y by A2, XBOOLE_0:def_5;
hence  x in Z by A3, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:44
for X, Y, Z being set st X \ Y c= Z holds
X c= Y \/ Z
proof
let X, Y, Z be set ; ::_thesis: ( X \ Y c= Z implies X c= Y \/ Z )
assume A1: for x being set st x in X \ Y holds
x in Z ; :: according to TARSKI:def_3 ::_thesis: X c= Y \/ Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y \/ Z )
assume  x in X ; ::_thesis: x in Y \/ Z
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  x in Y \/ Z by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:45
for X, Y being set st X c= Y holds
Y = X \/ (Y \ X)
proof
let X, Y be set ; ::_thesis: ( X c= Y implies Y = X \/ (Y \ X) )
assume A1: X c= Y ; ::_thesis: Y = X \/ (Y \ X)
now__::_thesis:_for_x_being_set_holds_
(_x_in_Y_iff_x_in_X_\/_(Y_\_X)_)
let x be set ; ::_thesis: ( x in Y iff x in X \/ (Y \ X) )
 ( x in Y iff ( x in X or x in Y \ X ) ) by A1, TARSKI:def_3, XBOOLE_0:def_5;
hence  ( x in Y iff x in X \/ (Y \ X) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  Y = X \/ (Y \ X) by TARSKI:1; ::_thesis: verum
end;

theorem :: XBOOLE_1:46
for X, Y being set holds X \ (X \/ Y) = {}
proof
let X, Y be set ; ::_thesis: X \ (X \/ Y) = {}
 X c= X \/ Y by Th7;
hence  X \ (X \/ Y) = {} by Lm1; ::_thesis: verum
end;

theorem Th47: :: XBOOLE_1:47
for X, Y being set holds X \ (X /\ Y) = X \ Y
proof
let X, Y be set ; ::_thesis: X \ (X /\ Y) = X \ Y
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_\_(X_/\_Y)_iff_x_in_X_\_Y_)
let x be set ; ::_thesis: ( x in X \ (X /\ Y) iff x in X \ Y )
 ( 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; ::_thesis: verum
end;
hence  X \ (X /\ Y) = X \ Y by TARSKI:1; ::_thesis: verum
end;

theorem :: XBOOLE_1:48
for X, Y being set holds X \ (X \ Y) = X /\ Y
proof
let X, Y be set ; ::_thesis: X \ (X \ Y) = X /\ Y
thus  for x being set st x in X \ (X \ Y) holds
x in X /\ Y :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X /\ Y c= X \ (X \ Y)
proof
let x be set ; ::_thesis: ( x in X \ (X \ Y) implies x in X /\ Y )
assume A1: x in X \ (X \ Y) ; ::_thesis: x in 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  x in X /\ Y by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  for x being set st x in X /\ Y holds
x in X \ (X \ Y) :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X /\ Y implies x in X \ (X \ Y) )
assume A3: x in X /\ Y ; ::_thesis: x in X \ (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  x in X \ (X \ Y) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem Th49: :: XBOOLE_1:49
for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ Z
proof
let X, Y, Z be set ; ::_thesis: X /\ (Y \ Z) = (X /\ Y) \ Z
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_/\_(Y_\_Z)_iff_x_in_(X_/\_Y)_\_Z_)
let x be set ; ::_thesis: ( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z )
 ( 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, XBOOLE_0:def_5;
hence  ( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z ) by XBOOLE_0:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X /\ (Y \ Z) = (X /\ Y) \ Z by TARSKI:1; ::_thesis: verum
end;

theorem Th50: :: XBOOLE_1:50
for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
proof
let X, Y, Z be set ; ::_thesis: X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
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  X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th49; ::_thesis: verum
end;

theorem Th51: :: XBOOLE_1:51
for X, Y being set holds (X /\ Y) \/ (X \ Y) = X
proof
let X, Y be set ; ::_thesis: (X /\ Y) \/ (X \ Y) = X
thus  (X /\ Y) \/ (X \ Y) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= (X /\ Y) \/ (X \ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) \/ (X \ Y) or x in X )
assume  x in (X /\ Y) \/ (X \ Y) ; ::_thesis: x in X
then  ( x in X /\ Y or x in X \ Y ) by XBOOLE_0:def_3;
hence  x in X by XBOOLE_0:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (X /\ Y) \/ (X \ Y) )
assume  x in X ; ::_thesis: x in (X /\ Y) \/ (X \ Y)
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  x in (X /\ Y) \/ (X \ Y) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th52: :: XBOOLE_1:52
for X, Y, Z being set holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
proof
let X, Y, Z be set ; ::_thesis: X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
thus  for x being set st x in X \ (Y \ Z) holds
x in (X \ Y) \/ (X /\ Z) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (X \ Y) \/ (X /\ Z) c= X \ (Y \ Z)
proof
let x be set ; ::_thesis: ( x in X \ (Y \ Z) implies x in (X \ Y) \/ (X /\ Z) )
assume A1: x in X \ (Y \ Z) ; ::_thesis: x in (X \ Y) \/ (X /\ 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, XBOOLE_0:def_5;
hence  x in (X \ Y) \/ (X /\ Z) by XBOOLE_0:def_3; ::_thesis: verum
end;
thus  for x being set st x in (X \ Y) \/ (X /\ Z) holds
x in X \ (Y \ Z) :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in (X \ Y) \/ (X /\ Z) implies x in X \ (Y \ Z) )
assume  x in (X \ Y) \/ (X /\ Z) ; ::_thesis: x in X \ (Y \ 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, XBOOLE_0:def_5;
then  not x in Y \ Z by XBOOLE_0:def_5;
hence  x in X \ (Y \ Z) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: XBOOLE_1:53
for X, Y, Z being set holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proof
let X, Y, Z be set ; ::_thesis: X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
 ( 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; :: according to XBOOLE_0:def_10 ::_thesis: (X \ Y) /\ (X \ Z) c= X \ (Y \/ Z)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \ Y) /\ (X \ Z) or x in X \ (Y \/ Z) )
assume A1: x in (X \ Y) /\ (X \ Z) ; ::_thesis: x in X \ (Y \/ 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  x in X \ (Y \/ Z) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: XBOOLE_1:54
for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z) by Lm2;

theorem Th55: :: XBOOLE_1:55
for X, Y being set holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proof
let X, Y be set ; ::_thesis: (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
 for x being set holds
( x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X) )
proof
let x be set ; ::_thesis: ( x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X) )
thus  ( x in (X \/ Y) \ (X /\ Y) implies x in (X \ Y) \/ (Y \ X) ) ::_thesis: ( x in (X \ Y) \/ (Y \ X) implies x in (X \/ Y) \ (X /\ Y) )
proof
assume A1: x in (X \/ Y) \ (X /\ Y) ; ::_thesis: x in (X \ Y) \/ (Y \ X)
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  x in (X \ Y) \/ (Y \ X) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume  x in (X \ Y) \/ (Y \ X) ; ::_thesis: x in (X \/ Y) \ (X /\ Y)
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, XBOOLE_0:def_4;
hence  x in (X \/ Y) \ (X /\ Y) by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X) by TARSKI:1; ::_thesis: verum
end;

Lm3:  for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & Y c< Z implies X c< Z )
assume that
A1: X c= Y and
A2: Y c< Z ; ::_thesis: X c< Z
 Y c= Z by A2, XBOOLE_0:def_8;
hence  ( X c= Z & X <> Z ) by A1, A2, Th1, XBOOLE_0:def_10; :: according to XBOOLE_0:def_8 ::_thesis: verum
end;

theorem :: XBOOLE_1:56
for X, Y, Z being set st X c< Y & Y c< Z holds
X c< Z
proof
let X, Y, Z be set ; ::_thesis: ( X c< Y & Y c< Z implies X c< Z )
assume that
A1: X c< Y and
A2: Y c< Z ; ::_thesis: X c< Z
 X c= Y by A1, XBOOLE_0:def_8;
hence  X c< Z by A2, Lm3; ::_thesis: verum
end;

theorem :: XBOOLE_1:57
for X, Y being set holds
( not X c< Y or not Y c< X ) ;

theorem :: XBOOLE_1:58
for X, Y, Z being set st X c< Y & Y c= Z holds
X c< Z
proof
let X, Y, Z be set ; ::_thesis: ( X c< Y & Y c= Z implies X c< Z )
assume that
A1: X c< Y and
A2: Y c= Z ; ::_thesis: X c< Z
 X c= Y by A1, XBOOLE_0:def_8;
hence  ( X c= Z & X <> Z ) by A1, A2, Th1, XBOOLE_0:def_10; :: according to XBOOLE_0:def_8 ::_thesis: verum
end;

theorem :: XBOOLE_1:59
for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z by Lm3;

theorem Th60: :: XBOOLE_1:60
for X, Y being set st X c= Y holds
not Y c< X
proof
let X, Y be set ; ::_thesis: ( X c= Y implies not Y c< X )
assume  ( X c= Y & Y c= X & X <> Y ) ; :: according to XBOOLE_0:def_8 ::_thesis: contradiction
hence  contradiction by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: XBOOLE_1:61
for X being set st X <> {} holds
{} c< X
proof
let X be set ; ::_thesis: ( X <> {} implies {} c< X )
assume A1: X <> {} ; ::_thesis: {} c< X
thus  {} c= X by Th2; :: according to XBOOLE_0:def_8 ::_thesis: not {} = X
thus  not {} = X by A1; ::_thesis: verum
end;

theorem :: XBOOLE_1:62
for X being set holds not X c< {}
proof
let X be set ; ::_thesis: not X c< {}
assume A1: X c< {} ; ::_thesis: contradiction
then  X c= {} by XBOOLE_0:def_8;
hence  contradiction by A1, Th3; ::_thesis: verum
end;

theorem Th63: :: XBOOLE_1:63
for X, Y, Z being set st X c= Y & Y misses Z holds
X misses Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & Y misses Z implies X misses Z )
assume  ( X c= Y & Y /\ Z = {} ) ; :: according to XBOOLE_0:def_7 ::_thesis: X misses Z
then  X /\ Z = {} by Th3, Th26;
hence  X misses Z by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: XBOOLE_1:64
for A, X, B, Y being set st A c= X & B c= Y & X misses Y holds
A misses B
proof
let A, X, B, Y be set ; ::_thesis: ( A c= X & B c= Y & X misses Y implies A misses B )
assume that
A1: A c= X and
A2: B c= Y and
A3: X misses Y ; ::_thesis: A misses B
 A misses Y by A1, A3, Th63;
hence  A misses B by A2, Th63; ::_thesis: verum
end;

theorem :: XBOOLE_1:65
for X being set holds X misses {}
proof
let X be set ; ::_thesis: X misses {}
assume  X meets {} ; ::_thesis: contradiction
then  ex x being set st
( x in X & x in {} ) by XBOOLE_0:3;
hence  contradiction ; ::_thesis: verum
end;

theorem :: XBOOLE_1:66
for X being set holds
( X meets X iff X <> {} )
proof
let X be set ; ::_thesis: ( X meets X iff X <> {} )
hereby  ::_thesis: ( X <> {} implies X meets X )
assume  X meets X ; ::_thesis: X <> {}
then  ex x being set st
( x in X & x in X ) by XBOOLE_0:3;
hence  X <> {} ; ::_thesis: verum
end;
assume  X <> {} ; ::_thesis: X meets X
then  X /\ X <> {} ;
hence  X meets X by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: XBOOLE_1:67
for X, Y, Z being set st X c= Y & X c= Z & Y misses Z holds
X = {}
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & X c= Z & Y misses Z implies X = {} )
assume  ( X c= Y & X c= Z & Y /\ Z = {} ) ; :: according to XBOOLE_0:def_7 ::_thesis: X = {}
hence  X = {} by Th3, Th19; ::_thesis: verum
end;

theorem Th68: :: XBOOLE_1:68
for Y, Z being set
for A being non empty set st A c= Y & A c= Z holds
Y meets Z
proof
let Y, Z be set ; ::_thesis: for A being non empty set st A c= Y & A c= Z holds
Y meets Z
let A be non empty set ; ::_thesis: ( A c= Y & A c= Z implies Y meets Z )
consider x being set  such that
A1: x in A by XBOOLE_0:def_1;
assume  ( A c= Y & A c= Z ) ; ::_thesis: Y meets Z
then  ( x in Y & x in Z ) by A1, TARSKI:def_3;
hence  Y meets Z by XBOOLE_0:3; ::_thesis: verum
end;

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

theorem Th70: :: XBOOLE_1:70
for X, Y, Z being set holds
( ( X meets Y or X meets Z ) iff X meets Y \/ Z )
proof
let X, Y, Z be set ; ::_thesis: ( ( X meets Y or X meets Z ) iff X meets Y \/ Z )
thus  ( not X meets Y \/ Z or X meets Y or X meets Z ) ::_thesis: ( ( X meets Y or X meets Z ) implies X meets Y \/ Z )
proof
assume  X meets Y \/ Z ; ::_thesis: ( X meets Y or X meets Z )
then consider x being set  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  ( X meets Y or X meets Z ) by XBOOLE_0:3; ::_thesis: verum
end;
A2: ( X meets Z implies X meets Y \/ Z )
proof
assume  X meets Z ; ::_thesis: X meets Y \/ Z
then consider x being set  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  X meets Y \/ Z by A3, XBOOLE_0:3; ::_thesis: verum
end;
 ( X meets Y implies X meets Y \/ Z )
proof
assume  X meets Y ; ::_thesis: X meets Y \/ Z
then consider x being set  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  X meets Y \/ Z by A5, XBOOLE_0:3; ::_thesis: verum
end;
hence  ( ( X meets Y or X meets Z ) implies X meets Y \/ Z ) by A2; ::_thesis: verum
end;

theorem :: XBOOLE_1:71
for X, Y, Z being set st X \/ Y = Z \/ Y & X misses Y & Z misses Y holds
X = Z
proof
let X, Y, Z be set ; ::_thesis: ( X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z )
assume that
A1: X \/ Y = Z \/ Y and
A2: X /\ Y = {} and
A3: Z /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: X = Z
thus  X c= Z :: according to XBOOLE_0:def_10 ::_thesis: Z c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume A4: x in X ; ::_thesis: x in Z
 X c= Z \/ Y by A1, Th7;
then A5: x in Z \/ Y by A4, TARSKI:def_3;
 not x in Y by A2, A4, XBOOLE_0:def_4;
hence  x in Z by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in X )
assume A6: x in Z ; ::_thesis: x in X
 Z c= X \/ Y by A1, Th7;
then A7: x in X \/ Y by A6, TARSKI:def_3;
 not x in Y by A3, A6, XBOOLE_0:def_4;
hence  x in X by A7, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: XBOOLE_1:72
for X9, Y9, X, Y being set st X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 holds
X = Y9
proof
let X9, Y9, X, Y be set ; ::_thesis: ( X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9 )
assume A1: X9 \/ Y9 = X \/ Y ; ::_thesis: ( not X misses X9 or not Y misses Y9 or X = Y9 )
assume  ( X misses X9 & Y misses Y9 ) ; ::_thesis: X = Y9
then A2: ( X /\ X9 = {} & Y /\ Y9 = {} ) by XBOOLE_0:def_7;
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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:73
for X, Y, Z being set st X c= Y \/ Z & X misses Z holds
X c= Y
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y \/ Z & X misses Z implies X c= Y )
assume that
A1: X c= Y \/ Z and
A2: X /\ Z = {} ; :: according to XBOOLE_0:def_7 ::_thesis: X c= Y
 X /\ (Y \/ Z) = X by A1, Th28;
then  (Y /\ X) \/ {} = X by A2, Th23;
hence  X c= Y by Th17; ::_thesis: verum
end;

theorem Th74: :: XBOOLE_1:74
for X, Y, Z being set st X meets Y /\ Z holds
X meets Y
proof
let X, Y, Z be set ; ::_thesis: ( X meets Y /\ Z implies X meets Y )
assume  X meets Y /\ Z ; ::_thesis: X meets Y
then consider x being set  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  X meets Y by A1, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: XBOOLE_1:75
for X, Y being set st X meets Y holds
X /\ Y meets Y
proof
let X, Y be set ; ::_thesis: ( X meets Y implies X /\ Y meets Y )
assume  X meets Y ; ::_thesis: X /\ Y meets Y
then consider x being set  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  X /\ Y meets Y by A2, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: XBOOLE_1:76
for Y, Z, X being set st Y misses Z holds
X /\ Y misses X /\ Z
proof
let Y, Z, X be set ; ::_thesis: ( Y misses Z implies X /\ Y misses X /\ Z )
assume  Y misses Z ; ::_thesis: X /\ Y misses X /\ Z
then  X /\ Z misses Y by Th74;
hence  X /\ Y misses X /\ Z by Th74; ::_thesis: verum
end;

theorem :: XBOOLE_1:77
for X, Y, Z being set st X meets Y & X c= Z holds
X meets Y /\ Z
proof
let X, Y, Z be set ; ::_thesis: ( X meets Y & X c= Z implies X meets Y /\ Z )
assume that
A1: X meets Y and
A2: X c= Z ; ::_thesis: X meets Y /\ Z
now__::_thesis:_not_X_/\_(Y_/\_Z)_=_{}
assume A3: X /\ (Y /\ Z) = {} ; ::_thesis: contradiction
X /\ Y = (X /\ Z) /\ Y by A2, Th28
.= {} by A3, Th16 ;
hence  contradiction by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  X meets Y /\ Z by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: XBOOLE_1:78
for X, Y, Z being set st X misses Y holds
X /\ (Y \/ Z) = X /\ Z
proof
let X, Y, Z be set ; ::_thesis: ( X misses Y implies X /\ (Y \/ Z) = X /\ Z )
assume  X misses Y ; ::_thesis: X /\ (Y \/ Z) = X /\ Z
then  X /\ Y = {} by XBOOLE_0:def_7;
hence X /\ (Y \/ Z) = {} \/ (X /\ Z) by Th23
.= X /\ Z ;
::_thesis: verum
end;

theorem Th79: :: XBOOLE_1:79
for X, Y being set holds X \ Y misses Y
proof
let X, Y be set ; ::_thesis: X \ Y misses Y
 for x being set holds not x in (X \ Y) /\ Y
proof
given x being set  such that A1: x in (X \ Y) /\ Y ; ::_thesis: contradiction
 ( x in X \ Y & x in Y ) by A1, XBOOLE_0:def_4;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (X \ Y) /\ Y = {} by XBOOLE_0:def_1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem :: XBOOLE_1:80
for X, Y, Z being set st X misses Y holds
X misses Y \ Z
proof
let X, Y, Z be set ; ::_thesis: ( X misses Y implies X misses Y \ Z )
assume A1: X misses Y ; ::_thesis: X misses Y \ Z
assume  X meets Y \ Z ; ::_thesis: contradiction
then consider x being set  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  contradiction by A1, A2, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: XBOOLE_1:81
for X, Y, Z being set st X misses Y \ Z holds
Y misses X \ Z
proof
let X, Y, Z be set ; ::_thesis: ( X misses Y \ Z implies Y misses X \ Z )
A1: ( X misses Y \ Z iff X /\ (Y \ Z) = {} ) by XBOOLE_0:def_7;
X /\ (Y \ Z) = (Y /\ X) \ Z by Th49
.= Y /\ (X \ Z) by Th49 ;
hence  ( X misses Y \ Z implies Y misses X \ Z ) by A1, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: XBOOLE_1:82
for X, Y being set holds X \ Y misses Y \ X
proof
let X, Y be set ; ::_thesis: X \ Y misses Y \ X
assume  X \ Y meets Y \ X ; ::_thesis: contradiction
then consider x being set  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  contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th83: :: XBOOLE_1:83
for X, Y being set holds
( X misses Y iff X \ Y = X )
proof
let X, Y be set ; ::_thesis: ( X misses Y iff X \ Y = X )
thus  ( X misses Y implies X \ Y = X ) ::_thesis: ( X \ Y = X implies X misses Y )
proof
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: X \ Y = X
thus  for x being set st x in X \ Y holds
x in X by XBOOLE_0:def_5; :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X c= X \ Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \ Y )
 ( x in X /\ Y or not x in X or not x in Y ) by XBOOLE_0:def_4;
hence  ( not x in X or x in X \ Y ) by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A2: X \ Y = X ; ::_thesis: X misses Y
 for x being set holds not x in X /\ Y
proof
given x being set  such that A3: x in X /\ Y ; ::_thesis: contradiction
 ( x in X & x in Y ) by A3, XBOOLE_0:def_4;
hence  contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X misses Y by XBOOLE_0:4; ::_thesis: verum
end;

theorem :: XBOOLE_1:84
for X, Y, Z being set st X meets Y & X misses Z holds
X meets Y \ Z
proof
let X, Y, Z be set ; ::_thesis: ( X meets Y & X misses Z implies X meets Y \ Z )
assume that
A1: X meets Y and
A2: X misses Z ; ::_thesis: X meets Y \ Z
X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th50
.= (X /\ Y) \ {} by A2, XBOOLE_0:def_7 ;
hence  X /\ (Y \ Z) <> {} by A1, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem :: XBOOLE_1:85
for X, Y, Z being set st X c= Y holds
X misses Z \ Y
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies X misses Z \ Y )
assume A1: X c= Y ; ::_thesis: X misses Z \ Y
thus X /\ (Z \ Y) = (Z /\ X) \ Y by Th49
.= Z /\ (X \ Y) by Th49
.= Z /\ {} by A1, Lm1
.= {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th86: :: XBOOLE_1:86
for X, Y, Z being set st X c= Y & X misses Z holds
X c= Y \ Z
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y & X misses Z implies X c= Y \ Z )
assume A1: ( X c= Y & X /\ Z = {} ) ; :: according to XBOOLE_0:def_7 ::_thesis: X c= Y \ Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y \ Z )
assume  x in X ; ::_thesis: x in Y \ Z
then  ( x in Y & not x in Z ) by A1, TARSKI:def_3, XBOOLE_0:def_4;
hence  x in Y \ Z by XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: XBOOLE_1:87
for Y, Z, X being set st Y misses Z holds
(X \ Y) \/ Z = (X \/ Z) \ Y
proof
let Y, Z, X be set ; ::_thesis: ( Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y )
assume A1: Y misses Z ; ::_thesis: (X \ Y) \/ Z = (X \/ Z) \ Y
thus (X \/ Z) \ Y = (X \ Y) \/ (Z \ Y) by Th42
.= (X \ Y) \/ Z by A1, Th83 ; ::_thesis: verum
end;

theorem Th88: :: XBOOLE_1:88
for X, Y being set st X misses Y holds
(X \/ Y) \ Y = X
proof
let X, Y be set ; ::_thesis: ( X misses Y implies (X \/ Y) \ Y = X )
assume A1: X misses Y ; ::_thesis: (X \/ Y) \ Y = X
thus (X \/ Y) \ Y = (X \ Y) \/ (Y \ Y) by Th42
.= (X \ Y) \/ {} by Lm1
.= X by A1, Th83 ; ::_thesis: verum
end;

theorem Th89: :: XBOOLE_1:89
for X, Y being set holds X /\ Y misses X \ Y
proof
let X, Y be set ; ::_thesis: X /\ Y misses X \ Y
now__::_thesis:_for_x_being_set_holds_
(_not_x_in_X_/\_Y_or_not_x_in_X_\_Y_)
let x be set ; ::_thesis: ( not x in X /\ Y or not x in X \ Y )
 ( not x in X or not x in Y or x in Y ) ;
hence  ( not x in X /\ Y or not x in X \ Y ) by XBOOLE_0:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X /\ Y misses X \ Y by XBOOLE_0:3; ::_thesis: verum
end;

theorem :: XBOOLE_1:90
for X, Y being set holds X \ (X /\ Y) misses Y
proof
let X, Y be set ; ::_thesis: X \ (X /\ Y) misses Y
 X \ (X /\ Y) = X \ Y by Th47;
hence  X \ (X /\ Y) misses Y by Th79; ::_thesis: verum
end;

theorem :: XBOOLE_1:91
for X, Y, Z being set holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
let X, Y, Z be set ; ::_thesis: (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
set S1 = X \ (Y \/ Z);
set S2 = Y \ (X \/ Z);
set S3 = Z \ (X \/ Y);
set S4 = (X /\ Y) /\ Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th42
.= ((X \ (Y \/ Z)) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th55
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (((X /\ Y) /\ Z) \/ (Z \ (X \/ Y))) by Th52
.= (((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ ((X /\ Y) /\ Z)) \/ (Z \ (X \/ Y)) by Th4
.= (((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ (X \/ Y)) by Th4
.= ((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th4
.= ((X \ (Y \/ Z)) \/ (X /\ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th16
.= (X \ ((Y \/ Z) \ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th52
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (X \/ Z)) \/ (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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:92
for X being set holds X \+\ X = {} by Lm1;

theorem Th93: :: XBOOLE_1:93
for X, Y being set holds X \/ Y = (X \+\ Y) \/ (X /\ Y)
proof
let X, Y be set ; ::_thesis: X \/ Y = (X \+\ Y) \/ (X /\ Y)
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 ; ::_thesis: verum
end;

Lm4:  for X, Y being set holds X /\ Y misses X \+\ Y
proof
let X, Y be set ; ::_thesis: X /\ Y misses X \+\ Y
 ( X /\ Y misses X \ Y & X /\ Y misses Y \ X ) by Th89;
hence  X /\ Y misses X \+\ Y by Th70; ::_thesis: verum
end;

Lm5:  for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y)
proof
let X, Y be set ; ::_thesis: X \+\ Y = (X \/ Y) \ (X /\ Y)
thus X \+\ Y = (X \ (X /\ Y)) \/ (Y \ X) by Th47
.= (X \ (X /\ Y)) \/ (Y \ (X /\ Y)) by Th47
.= (X \/ Y) \ (X /\ Y) by Th42 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:94
for X, Y being set holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
proof
let X, Y be set ; ::_thesis: X \/ Y = (X \+\ Y) \+\ (X /\ Y)
 X /\ Y misses X \+\ Y by Lm4;
then  ( (X \+\ Y) \ (X /\ Y) = X \+\ Y & (X /\ Y) \ (X \+\ Y) = X /\ Y ) by Th83;
hence  X \/ Y = (X \+\ Y) \+\ (X /\ Y) by Th93; ::_thesis: verum
end;

theorem :: XBOOLE_1:95
for X, Y being set holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
proof
let X, Y be set ; ::_thesis: X /\ Y = (X \+\ Y) \+\ (X \/ Y)
 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  X /\ Y = (X \+\ Y) \+\ (X \/ Y) by A1, Lm4, Th88; ::_thesis: verum
end;

theorem :: XBOOLE_1:96
for X, Y being set holds X \ Y c= X \+\ Y by Th7;

theorem :: XBOOLE_1:97
for X, Y, Z being set st X \ Y c= Z & Y \ X c= Z holds
X \+\ Y c= Z by Th8;

theorem :: XBOOLE_1:98
for X, Y being set holds X \/ Y = X \+\ (Y \ X)
proof
let X, Y be set ; ::_thesis: X \/ Y = X \+\ (Y \ X)
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  X \/ Y = X \+\ (Y \ X) by A1, Th39; ::_thesis: verum
end;

theorem :: XBOOLE_1:99
for X, Y, Z being set holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proof
let X, Y, Z be set ; ::_thesis: (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:100
for X, Y being set holds X \ Y = X \+\ (X /\ Y)
proof
let X, Y be set ; ::_thesis: X \ Y = X \+\ (X /\ Y)
 X /\ Y c= X by Th17;
then  (X /\ Y) \ X = {} by Lm1;
hence  X \ Y = X \+\ (X /\ Y) by Th47; ::_thesis: verum
end;

theorem :: XBOOLE_1:101
for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y) by Lm5;

theorem :: XBOOLE_1:102
for X, Y, Z being set holds X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)
proof
let X, Y, Z be set ; ::_thesis: X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)
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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:103
for X, Y being set holds X /\ Y misses X \+\ Y by Lm4;

theorem :: XBOOLE_1:104
for X, Y being set holds
( ( X c< Y or X = Y or Y c< X ) iff X,Y are_c=-comparable )
proof
let X, Y be set ; ::_thesis: ( ( X c< Y or X = Y or Y c< X ) iff X,Y are_c=-comparable )
thus  ( ( X c< Y or X = Y or Y c< X ) implies X,Y are_c=-comparable ) ::_thesis: ( not X,Y are_c=-comparable or X c< Y or X = Y or Y c< X )
proof
assume  ( X c< Y or X = Y or Y c< X ) ; ::_thesis: X,Y are_c=-comparable
hence  ( X c= Y or Y c= X ) by XBOOLE_0:def_8; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
assume  ( X c= Y or Y c= X ) ; :: according to XBOOLE_0:def_9 ::_thesis: ( X c< Y or X = Y or Y c< X )
hence  ( X c< Y or X = Y or Y c< X ) by XBOOLE_0:def_8; ::_thesis: verum
end;

begin

theorem :: XBOOLE_1:105
for X, Y being set st X c< Y holds
Y \ X <> {}
proof
let X, Y be set ; ::_thesis: ( X c< Y implies Y \ X <> {} )
assume A1: X c< Y ; ::_thesis: Y \ X <> {}
assume  Y \ X = {} ; ::_thesis: contradiction
then  Y c= X by Lm1;
hence  contradiction by A1, Th60; ::_thesis: verum
end;

theorem Th106: :: XBOOLE_1:106
for X, A, B being set st X c= A \ B holds
( X c= A & X misses B )
proof
let X, A, B be set ; ::_thesis: ( X c= A \ B implies ( X c= A & X misses B ) )
assume A1: X c= A \ B ; ::_thesis: ( X c= A & X misses B )
 A \ B c= A by Th36;
hence  X c= A by A1, Th1; ::_thesis: X misses B
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
not_x_in_B
let x be set ; ::_thesis: ( x in X implies not x in B )
assume  x in X ; ::_thesis: not x in B
then  x in A \ B by A1, TARSKI:def_3;
hence  not x in B by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X misses B by XBOOLE_0:3; ::_thesis: verum
end;

theorem :: XBOOLE_1:107
for X, A, B being set holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
proof
let X, A, B be set ; ::_thesis: ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
 A \+\ B = (A \/ B) \ (A /\ B) by Lm5;
hence  ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) ) by Th86, Th106; ::_thesis: verum
end;

theorem :: XBOOLE_1:108
for X, A, Y being set st X c= A holds
X /\ Y c= A
proof
let X, A, Y be set ; ::_thesis: ( X c= A implies X /\ Y c= A )
 X /\ Y c= X by Th17;
hence  ( X c= A implies X /\ Y c= A ) by Th1; ::_thesis: verum
end;

theorem Th109: :: XBOOLE_1:109
for X, A, Y being set st X c= A holds
X \ Y c= A
proof
let X, A, Y be set ; ::_thesis: ( X c= A implies X \ Y c= A )
 X \ Y c= X by Th36;
hence  ( X c= A implies X \ Y c= A ) by Th1; ::_thesis: verum
end;

theorem :: XBOOLE_1:110
for X, A, Y being set st X c= A & Y c= A holds
X \+\ Y c= A
proof
let X, A, Y be set ; ::_thesis: ( X c= A & Y c= A implies X \+\ Y c= A )
assume  ( X c= A & Y c= A ) ; ::_thesis: X \+\ Y c= A
then  ( X \ Y c= A & Y \ X c= A ) by Th109;
hence  X \+\ Y c= A by Th8; ::_thesis: verum
end;

theorem Th111: :: XBOOLE_1:111
for X, Z, Y being set holds (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
proof
let X, Z, Y be set ; ::_thesis: (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:112
for X, Z, Y being set holds (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
proof
let X, Z, Y be set ; ::_thesis: (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
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 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:113
for X, Y, Z, V being set holds ((X \/ Y) \/ Z) \/ V = X \/ ((Y \/ Z) \/ V)
proof
let X, Y, Z, V be set ; ::_thesis: ((X \/ Y) \/ Z) \/ V = X \/ ((Y \/ Z) \/ V)
((X \/ Y) \/ Z) \/ V = (X \/ Y) \/ (Z \/ V) by Th4
.= X \/ (Y \/ (Z \/ V)) by Th4
.= X \/ ((Y \/ Z) \/ V) by Th4 ;
hence  ((X \/ Y) \/ Z) \/ V = X \/ ((Y \/ Z) \/ V) ; ::_thesis: verum
end;

theorem :: XBOOLE_1:114
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 ; ::_thesis: ( A misses D & B misses D & C misses D implies (A \/ B) \/ C misses D )
assume  ( A misses D & B misses D ) ; ::_thesis: ( not C misses D or (A \/ B) \/ C misses D )
then A1: A \/ B misses D by Th70;
assume  C misses D ; ::_thesis: (A \/ B) \/ C misses D
hence  (A \/ B) \/ C misses D by A1, Th70; ::_thesis: verum
end;

theorem :: XBOOLE_1:115
for A being set holds not A c< {}
proof
let A be set ; ::_thesis: not A c< {}
assume A1: A c< {} ; ::_thesis: contradiction
then  A c= {} by XBOOLE_0:def_8;
hence  contradiction by A1, Th3; ::_thesis: verum
end;

theorem :: XBOOLE_1:116
for X, Y, Z being set holds X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
proof
let X, Y, Z be set ; ::_thesis: X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
thus X /\ (Y /\ Z) = ((X /\ X) /\ Y) /\ Z by Th16
.= (X /\ (X /\ Y)) /\ Z by Th16
.= (X /\ Y) /\ (X /\ Z) by Th16 ; ::_thesis: verum
end;

theorem :: XBOOLE_1:117
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 ; ::_thesis: ( C c= G implies P \ C = (P \ G) \/ (P /\ (G \ C)) )
assume  C c= G ; ::_thesis: P \ C = (P \ G) \/ (P /\ (G \ C))
then A1: P \ G c= P \ C by Th34;
thus  P \ C c= (P \ G) \/ (P /\ (G \ C)) :: according to XBOOLE_0:def_10 ::_thesis: (P \ G) \/ (P /\ (G \ C)) c= P \ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P \ C or x in (P \ G) \/ (P /\ (G \ C)) )
assume  x in P \ C ; ::_thesis: x in (P \ G) \/ (P /\ (G \ 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  x in (P \ G) \/ (P /\ (G \ C)) by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( P /\ (G \ C) = (P /\ G) \ C & (P /\ G) \ C c= P \ C ) by Th17, Th33, Th49;
hence  (P \ G) \/ (P /\ (G \ C)) c= P \ C by A1, Th8; ::_thesis: verum
end;