:: ZFMISC_1 semantic presentation

begin


registration
let x, y be set ;
cluster[x,y] ->  non empty ;
coherence
 not [x,y] is empty ;
end;

Lm1:  for x, X being set holds
( {x} c= X iff x in X )
proof
let x, X be set ; ::_thesis: ( {x} c= X iff x in X )
 x in {x} by TARSKI:def_1;
hence  ( {x} c= X implies x in X ) by TARSKI:def_3; ::_thesis: ( x in X implies {x} c= X )
assume A1: x in X ; ::_thesis: {x} c= X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x} or y in X )
thus  ( not y in {x} or y in X ) by A1, TARSKI:def_1; ::_thesis: verum
end;

Lm2:  for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x}
proof
let Y, X, x be set ; ::_thesis: ( Y c= X & not x in Y implies Y c= X \ {x} )
assume A1: ( Y c= X & not x in Y ) ; ::_thesis: Y c= X \ {x}
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in X \ {x} )
assume  y in Y ; ::_thesis: y in X \ {x}
then  ( y in X & not y in {x} ) by A1, TARSKI:def_1, TARSKI:def_3;
hence  y in X \ {x} by XBOOLE_0:def_5; ::_thesis: verum
end;

Lm3:  for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )
proof
let Y, x be set ; ::_thesis: ( Y c= {x} iff ( Y = {} or Y = {x} ) )
thus  ( not Y c= {x} or Y = {} or Y = {x} ) ::_thesis: ( ( Y = {} or Y = {x} ) implies Y c= {x} )
proof
assume A1: Y c= {x} ; ::_thesis: ( Y = {} or Y = {x} )
 ( x in Y or not x in Y ) ;
then  ( {x} c= Y or Y c= {x} \ {x} ) by A1, Lm1, Lm2;
then  ( {x} = Y or Y c= {} ) by A1, XBOOLE_0:def_10, XBOOLE_1:37;
hence  ( Y = {} or Y = {x} ) by XBOOLE_1:3; ::_thesis: verum
end;
thus  ( ( Y = {} or Y = {x} ) implies Y c= {x} ) by XBOOLE_1:2; ::_thesis: verum
end;

definition
let X be set ;
defpred S1[ set ] means $1 c= X;
func bool X ->  set  means :Def1: :: ZFMISC_1:def 1
 for Z being set holds
( Z in it iff Z c= X );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff Z c= X )
proof
consider M being set  such that
A1: ( X in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) ) and
 for X being set st X in M holds
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) and
 for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by TARSKI:3;
consider IT being set  such that
A2: for Y being set holds
( Y in IT iff ( Y in M & S1[Y] ) ) from XBOOLE_0:sch_1();
take  IT ; ::_thesis: for Z being set holds
( Z in IT iff Z c= X )
thus  for Z being set holds
( Z in IT iff Z c= X ) by A2, A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff Z c= X ) ) & ( for Z being set holds
( Z in b2 iff Z c= X ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def1 defines bool ZFMISC_1:def_1_:_
 for X being set
for b2 being set holds
( b2 = bool X iff for Z being set holds
( Z in b2 iff Z c= X ) );

definition
let X1, X2 be set ;
defpred S1[ set ] means  ex x, y being set st
( x in X1 & y in X2 & $1 = [x,y] );
func[:X1,X2:] ->  set  means :Def2: :: ZFMISC_1:def 2
 for z being set holds
( z in it iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) );
existence
 ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
proof
A1: X1 c= X1 \/ X2 by XBOOLE_1:7;
consider X being set  such that
A2: for z being set holds
( z in X iff ( z in bool (bool (X1 \/ X2)) & S1[z] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for z being set holds
( z in X iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
let z be set ; ::_thesis: ( z in X iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
thus  ( z in X implies ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) by A2; ::_thesis: ( ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) implies z in X )
given x, y being set  such that A3: x in X1 and
A4: y in X2 and
A5: z = [x,y] ; ::_thesis: z in X
 {x,y} c= X1 \/ X2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in X1 \/ X2 )
assume  z in {x,y} ; ::_thesis: z in X1 \/ X2
then  ( z = x or z = y ) by TARSKI:def_2;
hence  z in X1 \/ X2 by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
then A6: {x,y} in bool (X1 \/ X2) by Def1;
 {x} c= X1 by A3, Lm1;
then  {x} c= X1 \/ X2 by A1, XBOOLE_1:1;
then A7: {x} in bool (X1 \/ X2) by Def1;
 {{x,y},{x}} c= bool (X1 \/ X2)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {{x,y},{x}} or z in bool (X1 \/ X2) )
assume  z in {{x,y},{x}} ; ::_thesis: z in bool (X1 \/ X2)
hence  z in bool (X1 \/ X2) by A7, A6, TARSKI:def_2; ::_thesis: verum
end;
then  {{x,y},{x}} in bool (bool (X1 \/ X2)) by Def1;
hence  z in X by A2, A3, A4, A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for z being set holds
( z in b1 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) & ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines [: ZFMISC_1:def_2_:_
 for X1, X2 being set
for b3 being set holds
( b3 = [:X1,X2:] iff for z being set holds
( z in b3 iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) );

definition
let X1, X2, X3 be set ;
func[:X1,X2,X3:] ->  set  equals :: ZFMISC_1:def 3
[:[:X1,X2:],X3:];
coherence
 [:[:X1,X2:],X3:] is set ;
end;

:: deftheorem  defines [: ZFMISC_1:def_3_:_
 for X1, X2, X3 being set holds [:X1,X2,X3:] = [:[:X1,X2:],X3:];

definition
let X1, X2, X3, X4 be set ;
func[:X1,X2,X3,X4:] ->  set  equals :: ZFMISC_1:def 4
[:[:X1,X2,X3:],X4:];
coherence
 [:[:X1,X2,X3:],X4:] is set ;
end;

:: deftheorem  defines [: ZFMISC_1:def_4_:_
 for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];

begin

theorem :: ZFMISC_1:1
bool {} = {{}}
proof
now__::_thesis:_for_x_being_set_holds_
(_x_in_bool_{}_iff_x_in_{{}}_)
let x be set ; ::_thesis: ( x in bool {} iff x in {{}} )
 ( x c= {} iff x = {} ) by XBOOLE_1:3;
hence  ( x in bool {} iff x in {{}} ) by Def1, TARSKI:def_1; ::_thesis: verum
end;
hence  bool {} = {{}} by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:2
union {} = {}
proof
now__::_thesis:_for_x_being_set_holds_not_x_in_union_{}
given x being set  such that A1: x in union {} ; ::_thesis: contradiction
 ex X being set st
( x in X & X in {} ) by A1, TARSKI:def_4;
hence  contradiction ; ::_thesis: verum
end;
hence  union {} = {} by XBOOLE_0:7; ::_thesis: verum
end;

theorem Th3: :: ZFMISC_1:3
for x, y being set st {x} c= {y} holds
x = y
proof
let x, y be set ; ::_thesis: ( {x} c= {y} implies x = y )
 x in {x} by TARSKI:def_1;
then  ( {x} = {y} implies x = y ) by TARSKI:def_1;
hence  ( {x} c= {y} implies x = y ) by Lm3; ::_thesis: verum
end;

theorem Th4: :: ZFMISC_1:4
for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1
proof
let x, y1, y2 be set ; ::_thesis: ( {x} = {y1,y2} implies x = y1 )
assume  {x} = {y1,y2} ; ::_thesis: x = y1
then  y1 in {x} by TARSKI:def_2;
hence  x = y1 by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:5
for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( {x} = {y1,y2} implies y1 = y2 )
assume A1: {x} = {y1,y2} ; ::_thesis: y1 = y2
then  x = y1 by Th4;
hence  y1 = y2 by A1, Th4; ::_thesis: verum
end;

theorem Th6: :: ZFMISC_1:6
for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
 x1 in {x1,x2} by TARSKI:def_2;
hence  ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th7: :: ZFMISC_1:7
for x, y being set holds {x} c= {x,y}
proof
let x, y be set ; ::_thesis: {x} c= {x,y}
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x} or z in {x,y} )
assume  z in {x} ; ::_thesis: z in {x,y}
then  z = x by TARSKI:def_1;
hence  z in {x,y} by TARSKI:def_2; ::_thesis: verum
end;

Lm4:  for x, X being set st {x} \/ X c= X holds
x in X
proof
let x, X be set ; ::_thesis: ( {x} \/ X c= X implies x in X )
assume A1: {x} \/ X c= X ; ::_thesis: x in X
assume  not x in X ; ::_thesis: contradiction
then  not x in {x} \/ X by A1, TARSKI:def_3;
then  not x in {x} by XBOOLE_0:def_3;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:8
for x, y being set st {x} \/ {y} = {x} holds
x = y
proof
let x, y be set ; ::_thesis: ( {x} \/ {y} = {x} implies x = y )
assume  {x} \/ {y} = {x} ; ::_thesis: x = y
then  ( y in {x} or x in {y} ) by Lm4;
hence  x = y by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:9
for x, y being set holds {x} \/ {x,y} = {x,y}
proof
let x, y be set ; ::_thesis: {x} \/ {x,y} = {x,y}
 x in {x,y} by TARSKI:def_2;
hence  {x} \/ {x,y} = {x,y} by XBOOLE_1:12, Lm1; ::_thesis: verum
end;

Lm6:  for x, X being set st {x} misses X holds
not x in X
proof
let x, X be set ; ::_thesis: ( {x} misses X implies not x in X )
A1: x in {x} by TARSKI:def_1;
assume  ( {x} /\ X = {} & x in X ) ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
hence  contradiction by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: ZFMISC_1:10
for x, y being set st {x} misses {y} holds
x <> y
proof
let x, y be set ; ::_thesis: ( {x} misses {y} implies x <> y )
assume  {x} misses {y} ; ::_thesis: x <> y
then  not x in {y} by Lm6;
hence  x <> y by TARSKI:def_1; ::_thesis: verum
end;

Lm7:  for x, X being set st not x in X holds
{x} misses X
proof
let x, X be set ; ::_thesis: ( not x in X implies {x} misses X )
assume A1: not x in X ; ::_thesis: {x} misses X
thus  {x} /\ X c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= {x} /\ X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x} /\ X or y in {} )
assume  y in {x} /\ X ; ::_thesis: y in {}
then  ( y in {x} & y in X ) by XBOOLE_0:def_4;
hence  y in {} by A1, TARSKI:def_1; ::_thesis: verum
end;
thus  {} c= {x} /\ X by XBOOLE_1:2; ::_thesis: verum
end;

theorem Th11: :: ZFMISC_1:11
for x, y being set st x <> y holds
{x} misses {y}
proof
let x, y be set ; ::_thesis: ( x <> y implies {x} misses {y} )
assume  x <> y ; ::_thesis: {x} misses {y}
then  not x in {y} by TARSKI:def_1;
hence  {x} misses {y} by Lm7; ::_thesis: verum
end;

Lm8:  for X, x being set st X /\ {x} = {x} holds
x in X
proof
let X, x be set ; ::_thesis: ( X /\ {x} = {x} implies x in X )
assume  X /\ {x} = {x} ; ::_thesis: x in X
then  x in X /\ {x} by TARSKI:def_1;
hence  x in X by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: ZFMISC_1:12
for x, y being set st {x} /\ {y} = {x} holds
x = y
proof
let x, y be set ; ::_thesis: ( {x} /\ {y} = {x} implies x = y )
assume  {x} /\ {y} = {x} ; ::_thesis: x = y
then  ( x in {y} or y in {x} ) by Lm8;
hence  x = y by TARSKI:def_1; ::_thesis: verum
end;

Lm9:  for x, X being set st x in X holds
X /\ {x} = {x}
by XBOOLE_1:28, Lm1;

theorem :: ZFMISC_1:13
for x, y being set holds {x} /\ {x,y} = {x}
proof
let x, y be set ; ::_thesis: {x} /\ {x,y} = {x}
 x in {x,y} by TARSKI:def_2;
hence  {x} /\ {x,y} = {x} by XBOOLE_1:28, Lm1; ::_thesis: verum
end;

Lm10:  for x, X being set holds
( {x} \ X = {x} iff not x in X )
by Lm6, Lm7, XBOOLE_1:83;

theorem :: ZFMISC_1:14
for x, y being set holds
( {x} \ {y} = {x} iff x <> y )
proof
let x, y be set ; ::_thesis: ( {x} \ {y} = {x} iff x <> y )
 ( {x} \ {y} = {x} iff not x in {y} ) by Lm6, Lm7, XBOOLE_1:83;
hence  ( {x} \ {y} = {x} iff x <> y ) by TARSKI:def_1; ::_thesis: verum
end;

Lm11:  for x, X being set holds
( {x} \ X = {} iff x in X )
by Lm1, XBOOLE_1:37;

theorem :: ZFMISC_1:15
for x, y being set st {x} \ {y} = {} holds
x = y
proof
let x, y be set ; ::_thesis: ( {x} \ {y} = {} implies x = y )
assume  {x} \ {y} = {} ; ::_thesis: x = y
then  x in {y} by Lm1, XBOOLE_1:37;
hence  x = y by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:16
for x, y being set holds {x} \ {x,y} = {}
proof
let x, y be set ; ::_thesis: {x} \ {x,y} = {}
 x in {x,y} by TARSKI:def_2;
hence  {x} \ {x,y} = {} by Lm1, XBOOLE_1:37; ::_thesis: verum
end;

Lm12:  for x, y, X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )
proof
let x, y, X be set ; ::_thesis: ( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )
thus  ( {x,y} \ X = {x} implies ( not x in X & ( y in X or x = y ) ) ) ::_thesis: ( not x in X & ( y in X or x = y ) implies {x,y} \ X = {x} )
proof
assume A1: {x,y} \ X = {x} ; ::_thesis: ( not x in X & ( y in X or x = y ) )
then  x in {x,y} \ X by TARSKI:def_1;
hence  not x in X by XBOOLE_0:def_5; ::_thesis: ( y in X or x = y )
A2: y in {x,y} by TARSKI:def_2;
assume  not y in X ; ::_thesis: x = y
then  y in {x} by A1, A2, XBOOLE_0:def_5;
hence  x = y by TARSKI:def_1; ::_thesis: verum
end;
assume A3: ( not x in X & ( y in X or x = y ) ) ; ::_thesis: {x,y} \ X = {x}
 for z being set holds
( z in {x,y} \ X iff z = x )
proof
let z be set ; ::_thesis: ( z in {x,y} \ X iff z = x )
 ( z in {x,y} \ X iff ( z in {x,y} & not z in X ) ) by XBOOLE_0:def_5;
hence  ( z in {x,y} \ X iff z = x ) by A3, TARSKI:def_2; ::_thesis: verum
end;
hence  {x,y} \ X = {x} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:17
for x, y being set st x <> y holds
{x,y} \ {y} = {x}
proof
let x, y be set ; ::_thesis: ( x <> y implies {x,y} \ {y} = {x} )
assume  x <> y ; ::_thesis: {x,y} \ {y} = {x}
then A1: not x in {y} by TARSKI:def_1;
 y in {y} by TARSKI:def_1;
hence  {x,y} \ {y} = {x} by A1, Lm12; ::_thesis: verum
end;

theorem :: ZFMISC_1:18
for x, y being set st {x} c= {y} holds
x = y by Th3;

theorem :: ZFMISC_1:19
for z, x, y being set holds
( not {z} c= {x,y} or z = x or z = y )
proof
let z, x, y be set ; ::_thesis: ( not {z} c= {x,y} or z = x or z = y )
A1: z in {z} by TARSKI:def_1;
assume  {z} c= {x,y} ; ::_thesis: ( z = x or z = y )
then  z in {x,y} by A1, TARSKI:def_3;
hence  ( z = x or z = y ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th20: :: ZFMISC_1:20
for x, y, z being set st {x,y} c= {z} holds
x = z
proof
let x, y, z be set ; ::_thesis: ( {x,y} c= {z} implies x = z )
A1: x in {x,y} by TARSKI:def_2;
assume  {x,y} c= {z} ; ::_thesis: x = z
then  x in {z} by A1, TARSKI:def_3;
hence  x = z by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:21
for x, y, z being set st {x,y} c= {z} holds
{x,y} = {z}
proof
let x, y, z be set ; ::_thesis: ( {x,y} c= {z} implies {x,y} = {z} )
assume  {x,y} c= {z} ; ::_thesis: {x,y} = {z}
then  ( x = z & y = z ) by Th20;
hence  {x,y} = {z} by ENUMSET1:29; ::_thesis: verum
end;

Lm13:  for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x )
proof
let X, x be set ; ::_thesis: ( X <> {x} & X <> {} implies ex y being set st
( y in X & y <> x ) )
assume that
A1: X <> {x} and
A2: X <> {} ; ::_thesis: ex y being set st
( y in X & y <> x )
percases ( not x in X or x in X ) ;
supposeA3: not x in X ; ::_thesis: ex y being set st
( y in X & y <> x )
consider y being set  such that
A4: y in X by A2, XBOOLE_0:7;
take  y ; ::_thesis: ( y in X & y <> x )
thus  ( y in X & y <> x ) by A3, A4; ::_thesis: verum
end;
supposeA5: x in X ; ::_thesis: ex y being set st
( y in X & y <> x )
consider y being set  such that
A6: ( ( y in X & not y in {x} ) or ( y in {x} & not y in X ) ) by A1, TARSKI:1;
take  y ; ::_thesis: ( y in X & y <> x )
thus  ( y in X & y <> x ) by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

Lm14:  for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
proof
let Z, x1, x2 be set ; ::_thesis: ( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
thus  ( not Z c= {x1,x2} or Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ::_thesis: ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} )
proof
assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2} ; ::_thesis: Z = {x1,x2}
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_Z_implies_z_in_{x1,x2}_)_&_(_z_in_{x1,x2}_implies_z_in_Z_)_)
let z be set ; ::_thesis: ( ( z in Z implies z in {x1,x2} ) & ( z in {x1,x2} implies z in Z ) )
thus  ( z in Z implies z in {x1,x2} ) by A1, TARSKI:def_3; ::_thesis: ( z in {x1,x2} implies z in Z )
A5: now__::_thesis:_x1_in_Z
assume A6: not x1 in Z ; ::_thesis: contradiction
consider y being set  such that
A7: y in Z and
A8: y <> x2 by A2, A4, Lm13;
 y in {x1,x2} by A1, A7, TARSKI:def_3;
hence  contradiction by A6, A7, A8, TARSKI:def_2; ::_thesis: verum
end;
A9: now__::_thesis:_x2_in_Z
assume A10: not x2 in Z ; ::_thesis: contradiction
consider y being set  such that
A11: y in Z and
A12: y <> x1 by A2, A3, Lm13;
 y in {x1,x2} by A1, A11, TARSKI:def_3;
hence  contradiction by A10, A11, A12, TARSKI:def_2; ::_thesis: verum
end;
assume  z in {x1,x2} ; ::_thesis: z in Z
hence  z in Z by A5, A9, TARSKI:def_2; ::_thesis: verum
end;
hence  Z = {x1,x2} by TARSKI:1; ::_thesis: verum
end;
thus  ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} ) by Th7, XBOOLE_1:2; ::_thesis: verum
end;

theorem :: ZFMISC_1:22
for x1, x2, y1, y2 being set holds
( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )
assume  {x1,x2} c= {y1,y2} ; ::_thesis: ( x1 = y1 or x1 = y2 )
then  ( {x1,x2} = {} or {x1,x2} = {y1} or {x1,x2} = {y2} or {x1,x2} = {y1,y2} ) by Lm14;
hence  ( x1 = y1 or x1 = y2 ) by Th4, Th6; ::_thesis: verum
end;

theorem :: ZFMISC_1:23
for x, y being set st x <> y holds
{x} \+\ {y} = {x,y}
proof
let x, y be set ; ::_thesis: ( x <> y implies {x} \+\ {y} = {x,y} )
assume A1: x <> y ; ::_thesis: {x} \+\ {y} = {x,y}
 for z being set holds
( z in {x} \+\ {y} iff ( z = x or z = y ) )
proof
let z be set ; ::_thesis: ( z in {x} \+\ {y} iff ( z = x or z = y ) )
A2: ( z in {y} iff z = y ) by TARSKI:def_1;
 ( z in {x} iff z = x ) by TARSKI:def_1;
hence  ( z in {x} \+\ {y} iff ( z = x or z = y ) ) by A1, A2, XBOOLE_0:1; ::_thesis: verum
end;
hence  {x} \+\ {y} = {x,y} by TARSKI:def_2; ::_thesis: verum
end;

theorem :: ZFMISC_1:24
for x being set holds bool {x} = {{},{x}}
proof
let x be set ; ::_thesis: bool {x} = {{},{x}}
now__::_thesis:_for_y_being_set_holds_
(_y_in_bool_{x}_iff_y_in_{{},{x}}_)
let y be set ; ::_thesis: ( y in bool {x} iff y in {{},{x}} )
 ( y c= {x} iff ( y = {} or y = {x} ) ) by Lm3;
hence  ( y in bool {x} iff y in {{},{x}} ) by Def1, TARSKI:def_2; ::_thesis: verum
end;
hence  bool {x} = {{},{x}} by TARSKI:1; ::_thesis: verum
end;

Lm15:  for X, A being set st X in A holds
X c= union A
proof
let X, A be set ; ::_thesis: ( X in A implies X c= union A )
assume A1: X in A ; ::_thesis: X c= union A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in union A )
thus  ( not x in X or x in union A ) by A1, TARSKI:def_4; ::_thesis: verum
end;

theorem :: ZFMISC_1:25
for x being set holds union {x} = x
proof
let x be set ; ::_thesis: union {x} = x
A1: union {x} c= x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union {x} or y in x )
assume  y in union {x} ; ::_thesis: y in x
then  ex Y being set st
( y in Y & Y in {x} ) by TARSKI:def_4;
hence  y in x by TARSKI:def_1; ::_thesis: verum
end;
 x in {x} by TARSKI:def_1;
then  x c= union {x} by Lm15;
hence  union {x} = x by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm16:  for X, Y being set holds union {X,Y} = X \/ Y
proof
let X, Y be set ; ::_thesis: union {X,Y} = X \/ Y
 for x being set holds
( x in union {X,Y} iff ( x in X or x in Y ) )
proof
let x be set ; ::_thesis: ( x in union {X,Y} iff ( x in X or x in Y ) )
thus  ( not x in union {X,Y} or x in X or x in Y ) ::_thesis: ( ( x in X or x in Y ) implies x in union {X,Y} )
proof
assume  x in union {X,Y} ; ::_thesis: ( x in X or x in Y )
then  ex Z being set st
( x in Z & Z in {X,Y} ) by TARSKI:def_4;
hence  ( x in X or x in Y ) by TARSKI:def_2; ::_thesis: verum
end;
 ( X in {X,Y} & Y in {X,Y} ) by TARSKI:def_2;
hence  ( ( x in X or x in Y ) implies x in union {X,Y} ) by TARSKI:def_4; ::_thesis: verum
end;
hence  union {X,Y} = X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: ZFMISC_1:26
for x, y being set holds union {{x},{y}} = {x,y}
proof
let x, y be set ; ::_thesis: union {{x},{y}} = {x,y}
thus  union {{x},{y}} = {x} \/ {y} by Lm16
.= {x,y} by ENUMSET1:1 ; ::_thesis: verum
end;

Lm17:  for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
proof
let x, y, X, Y be set ; ::_thesis: ( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
thus  ( [x,y] in [:X,Y:] implies ( x in X & y in Y ) ) ::_thesis: ( x in X & y in Y implies [x,y] in [:X,Y:] )
proof
assume  [x,y] in [:X,Y:] ; ::_thesis: ( x in X & y in Y )
then  ex x1, y1 being set st
( x1 in X & y1 in Y & [x,y] = [x1,y1] ) by Def2;
hence  ( x in X & y in Y ) by XTUPLE_0:1; ::_thesis: verum
end;
thus  ( x in X & y in Y implies [x,y] in [:X,Y:] ) by Def2; ::_thesis: verum
end;

theorem :: ZFMISC_1:27
canceled;

theorem :: ZFMISC_1:28
for x, y, x1, y1 being set holds
( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )
proof
let x, y, x1, y1 be set ; ::_thesis: ( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )
 ( x = x1 & y = y1 iff ( x in {x1} & y in {y1} ) ) by TARSKI:def_1;
hence  ( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) ) by Lm17; ::_thesis: verum
end;

theorem :: ZFMISC_1:29
for x, y being set holds [:{x},{y}:] = {[x,y]}
proof
let x, y be set ; ::_thesis: [:{x},{y}:] = {[x,y]}
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_[:{x},{y}:]_implies_z_in_{[x,y]}_)_&_(_z_in_{[x,y]}_implies_z_in_[:{x},{y}:]_)_)
let z be set ; ::_thesis: ( ( z in [:{x},{y}:] implies z in {[x,y]} ) & ( z in {[x,y]} implies z in [:{x},{y}:] ) )
thus  ( z in [:{x},{y}:] implies z in {[x,y]} ) ::_thesis: ( z in {[x,y]} implies z in [:{x},{y}:] )
proof
assume  z in [:{x},{y}:] ; ::_thesis: z in {[x,y]}
then consider x1, y1 being set  such that
A1: ( x1 in {x} & y1 in {y} ) and
A2: z = [x1,y1] by Def2;
 ( x1 = x & y1 = y ) by A1, TARSKI:def_1;
hence  z in {[x,y]} by A2, TARSKI:def_1; ::_thesis: verum
end;
assume  z in {[x,y]} ; ::_thesis: z in [:{x},{y}:]
then A3: z = [x,y] by TARSKI:def_1;
 ( x in {x} & y in {y} ) by TARSKI:def_1;
hence  z in [:{x},{y}:] by A3, Lm17; ::_thesis: verum
end;
hence  [:{x},{y}:] = {[x,y]} by TARSKI:1; ::_thesis: verum
end;

theorem Th30: :: ZFMISC_1:30
for x, y, z being set holds
( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )
proof
let x, y, z be set ; ::_thesis: ( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )
now__::_thesis:_for_v_being_set_holds_
(_(_v_in_[:{x},{y,z}:]_implies_v_in_{[x,y],[x,z]}_)_&_(_v_in_{[x,y],[x,z]}_implies_v_in_[:{x},{y,z}:]_)_)
let v be set ; ::_thesis: ( ( v in [:{x},{y,z}:] implies v in {[x,y],[x,z]} ) & ( v in {[x,y],[x,z]} implies v in [:{x},{y,z}:] ) )
A1: z in {y,z} by TARSKI:def_2;
thus  ( v in [:{x},{y,z}:] implies v in {[x,y],[x,z]} ) ::_thesis: ( v in {[x,y],[x,z]} implies v in [:{x},{y,z}:] )
proof
assume  v in [:{x},{y,z}:] ; ::_thesis: v in {[x,y],[x,z]}
then consider x1, y1 being set  such that
A2: x1 in {x} and
A3: y1 in {y,z} and
A4: v = [x1,y1] by Def2;
A5: ( y1 = y or y1 = z ) by A3, TARSKI:def_2;
 x1 = x by A2, TARSKI:def_1;
hence  v in {[x,y],[x,z]} by A4, A5, TARSKI:def_2; ::_thesis: verum
end;
assume  v in {[x,y],[x,z]} ; ::_thesis: v in [:{x},{y,z}:]
then A6: ( v = [x,y] or v = [x,z] ) by TARSKI:def_2;
 ( x in {x} & y in {y,z} ) by TARSKI:def_1, TARSKI:def_2;
hence  v in [:{x},{y,z}:] by A6, A1, Lm17; ::_thesis: verum
end;
hence  [:{x},{y,z}:] = {[x,y],[x,z]} by TARSKI:1; ::_thesis: [:{x,y},{z}:] = {[x,z],[y,z]}
now__::_thesis:_for_v_being_set_holds_
(_(_v_in_[:{x,y},{z}:]_implies_v_in_{[x,z],[y,z]}_)_&_(_v_in_{[x,z],[y,z]}_implies_v_in_[:{x,y},{z}:]_)_)
let v be set ; ::_thesis: ( ( v in [:{x,y},{z}:] implies v in {[x,z],[y,z]} ) & ( v in {[x,z],[y,z]} implies v in [:{x,y},{z}:] ) )
A7: z in {z} by TARSKI:def_1;
thus  ( v in [:{x,y},{z}:] implies v in {[x,z],[y,z]} ) ::_thesis: ( v in {[x,z],[y,z]} implies v in [:{x,y},{z}:] )
proof
assume  v in [:{x,y},{z}:] ; ::_thesis: v in {[x,z],[y,z]}
then consider x1, y1 being set  such that
A8: x1 in {x,y} and
A9: y1 in {z} and
A10: v = [x1,y1] by Def2;
A11: ( x1 = x or x1 = y ) by A8, TARSKI:def_2;
 y1 = z by A9, TARSKI:def_1;
hence  v in {[x,z],[y,z]} by A10, A11, TARSKI:def_2; ::_thesis: verum
end;
assume  v in {[x,z],[y,z]} ; ::_thesis: v in [:{x,y},{z}:]
then A12: ( v = [x,z] or v = [y,z] ) by TARSKI:def_2;
 ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
hence  v in [:{x,y},{z}:] by A12, A7, Lm17; ::_thesis: verum
end;
hence  [:{x,y},{z}:] = {[x,z],[y,z]} by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:31
for x, X being set holds
( {x} c= X iff x in X ) by Lm1;

theorem Th32: :: ZFMISC_1:32
for x1, x2, Z being set holds
( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )
proof
let x1, x2, Z be set ; ::_thesis: ( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )
 ( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def_2;
hence  ( {x1,x2} c= Z implies ( x1 in Z & x2 in Z ) ) by TARSKI:def_3; ::_thesis: ( x1 in Z & x2 in Z implies {x1,x2} c= Z )
assume A1: ( x1 in Z & x2 in Z ) ; ::_thesis: {x1,x2} c= Z
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x1,x2} or z in Z )
assume  z in {x1,x2} ; ::_thesis: z in Z
hence  z in Z by A1, TARSKI:def_2; ::_thesis: verum
end;

theorem :: ZFMISC_1:33
for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) ) by Lm3;

theorem :: ZFMISC_1:34
for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x} by Lm2;

theorem :: ZFMISC_1:35
for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x ) by Lm13;

theorem :: ZFMISC_1:36
for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) ) by Lm14;

theorem Th37: :: ZFMISC_1:37
for z, X, Y being set holds
( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
proof
let z, X, Y be set ; ::_thesis: ( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
assume A1: {z} = X \/ Y ; ::_thesis: ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
 ( X <> {} or Y <> {} ) by A1;
hence  ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by A1, Lm3, XBOOLE_1:7; ::_thesis: verum
end;

theorem :: ZFMISC_1:38
for z, X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}
proof
let z, X, Y be set ; ::_thesis: ( {z} = X \/ Y & X <> Y & not X = {} implies Y = {} )
assume  {z} = X \/ Y ; ::_thesis: ( not X <> Y or X = {} or Y = {} )
then  ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by Th37;
hence  ( not X <> Y or X = {} or Y = {} ) ; ::_thesis: verum
end;

theorem :: ZFMISC_1:39
for x, X being set st {x} \/ X c= X holds
x in X by Lm4;

theorem :: ZFMISC_1:40
for x, X being set st x in X holds
{x} \/ X = X by XBOOLE_1:12, Lm1;

theorem :: ZFMISC_1:41
for x, y, Z being set st {x,y} \/ Z c= Z holds
x in Z
proof
let x, y, Z be set ; ::_thesis: ( {x,y} \/ Z c= Z implies x in Z )
assume A1: {x,y} \/ Z c= Z ; ::_thesis: x in Z
assume  not x in Z ; ::_thesis: contradiction
then  not x in {x,y} \/ Z by A1, TARSKI:def_3;
then  not x in {x,y} by XBOOLE_0:def_3;
hence  contradiction by TARSKI:def_2; ::_thesis: verum
end;

theorem :: ZFMISC_1:42
for x, Z, y being set st x in Z & y in Z holds
{x,y} \/ Z = Z by XBOOLE_1:12, Th32;

theorem :: ZFMISC_1:43
for x, X being set holds {x} \/ X <> {} ;

theorem :: ZFMISC_1:44
for x, y, X being set holds {x,y} \/ X <> {} ;

theorem :: ZFMISC_1:45
for X, x being set st X /\ {x} = {x} holds
x in X by Lm8;

theorem :: ZFMISC_1:46
for x, X being set st x in X holds
X /\ {x} = {x} by XBOOLE_1:28, Lm1;

theorem :: ZFMISC_1:47
for x, Z, y being set st x in Z & y in Z holds
{x,y} /\ Z = {x,y} by XBOOLE_1:28, Th32;

theorem :: ZFMISC_1:48
for x, X being set st {x} misses X holds
not x in X by Lm6;

theorem Th49: :: ZFMISC_1:49
for x, y, Z being set st {x,y} misses Z holds
not x in Z
proof
let x, y, Z be set ; ::_thesis: ( {x,y} misses Z implies not x in Z )
A1: x in {x,y} by TARSKI:def_2;
assume  ( {x,y} /\ Z = {} & x in Z ) ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
hence  contradiction by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: ZFMISC_1:50
for x, X being set st not x in X holds
{x} misses X by Lm7;

theorem Th51: :: ZFMISC_1:51
for x, Z, y being set st not x in Z & not y in Z holds
{x,y} misses Z
proof
let x, Z, y be set ; ::_thesis: ( not x in Z & not y in Z implies {x,y} misses Z )
assume A1: ( not x in Z & not y in Z ) ; ::_thesis: {x,y} misses Z
assume  {x,y} meets Z ; ::_thesis: contradiction
then consider z being set  such that
A2: z in {x,y} /\ Z by XBOOLE_0:4;
 ( z in {x,y} & z in Z ) by A2, XBOOLE_0:def_4;
hence  contradiction by A1, TARSKI:def_2; ::_thesis: verum
end;

theorem :: ZFMISC_1:52
for x, X being set holds
( {x} misses X or {x} /\ X = {x} ) by Lm7, Lm9;

theorem :: ZFMISC_1:53
for x, y, X being set holds
( not {x,y} /\ X = {x} or not y in X or x = y )
proof
let x, y, X be set ; ::_thesis: ( not {x,y} /\ X = {x} or not y in X or x = y )
A1: y in {x,y} by TARSKI:def_2;
assume  ( {x,y} /\ X = {x} & y in X ) ; ::_thesis: x = y
then  y in {x} by A1, XBOOLE_0:def_4;
hence  x = y by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:54
for x, X, y being set st x in X & ( not y in X or x = y ) holds
{x,y} /\ X = {x}
proof
let x, X, y be set ; ::_thesis: ( x in X & ( not y in X or x = y ) implies {x,y} /\ X = {x} )
assume A1: ( x in X & ( not y in X or x = y ) ) ; ::_thesis: {x,y} /\ X = {x}
 for z being set holds
( z in {x,y} /\ X iff z = x )
proof
let z be set ; ::_thesis: ( z in {x,y} /\ X iff z = x )
 ( z in {x,y} /\ X iff ( z in {x,y} & z in X ) ) by XBOOLE_0:def_4;
hence  ( z in {x,y} /\ X iff z = x ) by A1, TARSKI:def_2; ::_thesis: verum
end;
hence  {x,y} /\ X = {x} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:55
for x, y, X being set st {x,y} /\ X = {x,y} holds
x in X
proof
let x, y, X be set ; ::_thesis: ( {x,y} /\ X = {x,y} implies x in X )
assume  {x,y} /\ X = {x,y} ; ::_thesis: x in X
then  ( ( x in {x,y} /\ X & y in {x,y} /\ X ) or ( x in X /\ {x,y} & y in X /\ {x,y} ) ) by TARSKI:def_2;
hence  x in X by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th56: :: ZFMISC_1:56
for z, X, x being set holds
( z in X \ {x} iff ( z in X & z <> x ) )
proof
let z, X, x be set ; ::_thesis: ( z in X \ {x} iff ( z in X & z <> x ) )
 ( z in X \ {x} iff ( z in X & not z in {x} ) ) by XBOOLE_0:def_5;
hence  ( z in X \ {x} iff ( z in X & z <> x ) ) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th57: :: ZFMISC_1:57
for X, x being set holds
( X \ {x} = X iff not x in X )
proof
let X, x be set ; ::_thesis: ( X \ {x} = X iff not x in X )
 ( X \ {x} = X iff X misses {x} ) by XBOOLE_1:83;
hence  ( X \ {x} = X iff not x in X ) by Lm6, Lm7; ::_thesis: verum
end;

theorem :: ZFMISC_1:58
for X, x being set holds
( not X \ {x} = {} or X = {} or X = {x} )
proof
let X, x be set ; ::_thesis: ( not X \ {x} = {} or X = {} or X = {x} )
assume  X \ {x} = {} ; ::_thesis: ( X = {} or X = {x} )
then  X c= {x} by XBOOLE_1:37;
hence  ( X = {} or X = {x} ) by Lm3; ::_thesis: verum
end;

theorem :: ZFMISC_1:59
for x, X being set holds
( {x} \ X = {x} iff not x in X ) by Lm6, Lm7, XBOOLE_1:83;

theorem :: ZFMISC_1:60
for x, X being set holds
( {x} \ X = {} iff x in X ) by Lm1, XBOOLE_1:37;

theorem :: ZFMISC_1:61
for x, X being set holds
( {x} \ X = {} or {x} \ X = {x} ) by Lm10, Lm11;

theorem :: ZFMISC_1:62
for x, y, X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) ) by Lm12;

theorem :: ZFMISC_1:63
for x, y, X being set holds
( {x,y} \ X = {x,y} iff ( not x in X & not y in X ) ) by Th49, Th51, XBOOLE_1:83;

theorem Th64: :: ZFMISC_1:64
for x, y, X being set holds
( {x,y} \ X = {} iff ( x in X & y in X ) )
proof
let x, y, X be set ; ::_thesis: ( {x,y} \ X = {} iff ( x in X & y in X ) )
 ( {x,y} \ X = {} iff {x,y} c= X ) by XBOOLE_1:37;
hence  ( {x,y} \ X = {} iff ( x in X & y in X ) ) by Th32; ::_thesis: verum
end;

theorem :: ZFMISC_1:65
for x, y, X being set holds
( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )
proof
let x, y, X be set ; ::_thesis: ( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )
assume that
A1: {x,y} \ X <> {} and
A2: {x,y} \ X <> {x} and
A3: {x,y} \ X <> {y} ; ::_thesis: {x,y} \ X = {x,y}
A4: ( ( not x in X & x <> y ) or y in X ) by A3, Lm12;
 ( x in X or ( not y in X & x <> y ) ) by A2, Lm12;
hence  {x,y} \ X = {x,y} by A1, A4, Th51, XBOOLE_1:83, Th64; ::_thesis: verum
end;

theorem :: ZFMISC_1:66
for X, x, y being set holds
( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) )
proof
let X, x, y be set ; ::_thesis: ( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) )
 ( X \ {x,y} = {} iff X c= {x,y} ) by XBOOLE_1:37;
hence  ( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) ) by Lm14; ::_thesis: verum
end;

theorem :: ZFMISC_1:67
for A, B being set st A c= B holds
bool A c= bool B
proof
let A, B be set ; ::_thesis: ( A c= B implies bool A c= bool B )
assume A1: A c= B ; ::_thesis: bool A c= bool B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool A or x in bool B )
assume  x in bool A ; ::_thesis: x in bool B
then  x c= A by Def1;
then  x c= B by A1, XBOOLE_1:1;
hence  x in bool B by Def1; ::_thesis: verum
end;

theorem :: ZFMISC_1:68
for A being set holds {A} c= bool A
proof
let A be set ; ::_thesis: {A} c= bool A
 A in bool A by Def1;
hence  {A} c= bool A by Lm1; ::_thesis: verum
end;

theorem :: ZFMISC_1:69
for A, B being set holds (bool A) \/ (bool B) c= bool (A \/ B)
proof
let A, B be set ; ::_thesis: (bool A) \/ (bool B) c= bool (A \/ B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (bool A) \/ (bool B) or x in bool (A \/ B) )
assume  x in (bool A) \/ (bool B) ; ::_thesis: x in bool (A \/ B)
then  ( x in bool A or x in bool B ) by XBOOLE_0:def_3;
then A1: ( x c= A or x c= B ) by Def1;
 ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
then  x c= A \/ B by A1, XBOOLE_1:1;
hence  x in bool (A \/ B) by Def1; ::_thesis: verum
end;

theorem :: ZFMISC_1:70
for A, B being set st (bool A) \/ (bool B) = bool (A \/ B) holds
A,B are_c=-comparable
proof
let A, B be set ; ::_thesis: ( (bool A) \/ (bool B) = bool (A \/ B) implies A,B are_c=-comparable )
assume A1: (bool A) \/ (bool B) = bool (A \/ B) ; ::_thesis: A,B are_c=-comparable
 A \/ B in bool (A \/ B) by Def1;
then  ( A \/ B in bool A or A \/ B in bool B ) by A1, XBOOLE_0:def_3;
then A2: ( A \/ B c= A or A \/ B c= B ) by Def1;
 ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
hence  ( A c= B or B c= A ) by A2, XBOOLE_0:def_10; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;

theorem :: ZFMISC_1:71
for A, B being set holds bool (A /\ B) = (bool A) /\ (bool B)
proof
let A, B be set ; ::_thesis: bool (A /\ B) = (bool A) /\ (bool B)
now__::_thesis:_for_x_being_set_holds_
(_x_in_bool_(A_/\_B)_iff_x_in_(bool_A)_/\_(bool_B)_)
let x be set ; ::_thesis: ( x in bool (A /\ B) iff x in (bool A) /\ (bool B) )
 ( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
then  ( ( x c= A & x c= B ) iff x c= A /\ B ) by XBOOLE_1:1, XBOOLE_1:19;
then  ( ( x in bool A & x in bool B ) iff x in bool (A /\ B) ) by Def1;
hence  ( x in bool (A /\ B) iff x in (bool A) /\ (bool B) ) by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  bool (A /\ B) = (bool A) /\ (bool B) by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:72
for A, B being set holds bool (A \ B) c= {{}} \/ ((bool A) \ (bool B))
proof
let A, B be set ; ::_thesis: bool (A \ B) c= {{}} \/ ((bool A) \ (bool B))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool (A \ B) or x in {{}} \/ ((bool A) \ (bool B)) )
assume  x in bool (A \ B) ; ::_thesis: x in {{}} \/ ((bool A) \ (bool B))
then A1: x c= A \ B by Def1;
then  x misses B by XBOOLE_1:63, XBOOLE_1:79;
then  ( A \ B c= A & x /\ B = {} ) by XBOOLE_0:def_7, XBOOLE_1:36;
then  ( x = {} or ( x c= A & not x c= B ) ) by A1, XBOOLE_1:1, XBOOLE_1:28;
then  ( x in {{}} or ( x in bool A & not x in bool B ) ) by Def1, TARSKI:def_1;
then  ( x in {{}} or x in (bool A) \ (bool B) ) by XBOOLE_0:def_5;
hence  x in {{}} \/ ((bool A) \ (bool B)) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: ZFMISC_1:73
for A, B being set holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proof
let A, B be set ; ::_thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (bool (A \ B)) \/ (bool (B \ A)) or x in bool (A \+\ B) )
assume  x in (bool (A \ B)) \/ (bool (B \ A)) ; ::_thesis: x in bool (A \+\ B)
then  ( x in bool (A \ B) or x in bool (B \ A) ) by XBOOLE_0:def_3;
then A1: ( x c= A \ B or x c= B \ A ) by Def1;
 x c= (A \ B) \/ (B \ A)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in (A \ B) \/ (B \ A) )
assume  z in x ; ::_thesis: z in (A \ B) \/ (B \ A)
then  ( z in A \ B or z in B \ A ) by A1, TARSKI:def_3;
hence  z in (A \ B) \/ (B \ A) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in bool (A \+\ B) by Def1; ::_thesis: verum
end;

theorem :: ZFMISC_1:74
for X, A being set st X in A holds
X c= union A by Lm15;

theorem :: ZFMISC_1:75
for X, Y being set holds union {X,Y} = X \/ Y by Lm16;

theorem :: ZFMISC_1:76
for A, Z being set st ( for X being set st X in A holds
X c= Z ) holds
union A c= Z
proof
let A, Z be set ; ::_thesis: ( ( for X being set st X in A holds
X c= Z ) implies union A c= Z )
assume A1: for X being set st X in A holds
X c= Z ; ::_thesis: union A c= Z
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union A or y in Z )
assume  y in union A ; ::_thesis: y in Z
then consider Y being set  such that
A2: y in Y and
A3: Y in A by TARSKI:def_4;
 Y c= Z by A1, A3;
hence  y in Z by A2, TARSKI:def_3; ::_thesis: verum
end;

theorem Th77: :: ZFMISC_1:77
for A, B being set st A c= B holds
union A c= union B
proof
let A, B be set ; ::_thesis: ( A c= B implies union A c= union B )
assume A1: A c= B ; ::_thesis: union A c= union B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union A or x in union B )
assume  x in union A ; ::_thesis: x in union B
then consider Y being set  such that
A2: x in Y and
A3: Y in A by TARSKI:def_4;
 Y in B by A1, A3, TARSKI:def_3;
hence  x in union B by A2, TARSKI:def_4; ::_thesis: verum
end;

theorem :: ZFMISC_1:78
for A, B being set holds union (A \/ B) = (union A) \/ (union B)
proof
let A, B be set ; ::_thesis: union (A \/ B) = (union A) \/ (union B)
A1: union (A \/ B) c= (union A) \/ (union B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A \/ B) or x in (union A) \/ (union B) )
assume  x in union (A \/ B) ; ::_thesis: x in (union A) \/ (union B)
then consider Y being set  such that
A2: x in Y and
A3: Y in A \/ B by TARSKI:def_4;
 ( Y in A or Y in B ) by A3, XBOOLE_0:def_3;
then  ( x in union A or x in union B ) by A2, TARSKI:def_4;
hence  x in (union A) \/ (union B) by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( union A c= union (A \/ B) & union B c= union (A \/ B) ) by Th77, XBOOLE_1:7;
then  (union A) \/ (union B) c= union (A \/ B) by XBOOLE_1:8;
hence  union (A \/ B) = (union A) \/ (union B) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th79: :: ZFMISC_1:79
for A, B being set holds union (A /\ B) c= (union A) /\ (union B)
proof
let A, B be set ; ::_thesis: union (A /\ B) c= (union A) /\ (union B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A /\ B) or x in (union A) /\ (union B) )
assume  x in union (A /\ B) ; ::_thesis: x in (union A) /\ (union B)
then consider Y being set  such that
A1: x in Y and
A2: Y in A /\ B by TARSKI:def_4;
 Y in B by A2, XBOOLE_0:def_4;
then A3: x in union B by A1, TARSKI:def_4;
 Y in A by A2, XBOOLE_0:def_4;
then  x in union A by A1, TARSKI:def_4;
hence  x in (union A) /\ (union B) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th80: :: ZFMISC_1:80
for A, B being set st ( for X being set st X in A holds
X misses B ) holds
union A misses B
proof
let A, B be set ; ::_thesis: ( ( for X being set st X in A holds
X misses B ) implies union A misses B )
assume A1: for X being set st X in A holds
X misses B ; ::_thesis: union A misses B
assume  union A meets B ; ::_thesis: contradiction
then consider z being set  such that
A2: z in (union A) /\ B by XBOOLE_0:4;
 z in union A by A2, XBOOLE_0:def_4;
then consider X being set  such that
A3: z in X and
A4: X in A by TARSKI:def_4;
 z in B by A2, XBOOLE_0:def_4;
then  z in X /\ B by A3, XBOOLE_0:def_4;
hence  contradiction by A1, A4, XBOOLE_0:4; ::_thesis: verum
end;

theorem :: ZFMISC_1:81
for A being set holds union (bool A) = A
proof
let A be set ; ::_thesis: union (bool A) = A
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_union_(bool_A)_implies_x_in_A_)_&_(_x_in_A_implies_x_in_union_(bool_A)_)_)
let x be set ; ::_thesis: ( ( x in union (bool A) implies x in A ) & ( x in A implies x in union (bool A) ) )
thus  ( x in union (bool A) implies x in A ) ::_thesis: ( x in A implies x in union (bool A) )
proof
assume  x in union (bool A) ; ::_thesis: x in A
then consider X being set  such that
A1: x in X and
A2: X in bool A by TARSKI:def_4;
 X c= A by A2, Def1;
hence  x in A by A1, TARSKI:def_3; ::_thesis: verum
end;
assume  x in A ; ::_thesis: x in union (bool A)
then  {x} c= A by Lm1;
then A3: {x} in bool A by Def1;
 x in {x} by TARSKI:def_1;
hence  x in union (bool A) by A3, TARSKI:def_4; ::_thesis: verum
end;
hence  union (bool A) = A by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:82
for A being set holds A c= bool (union A)
proof
let A be set ; ::_thesis: A c= bool (union A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in bool (union A) )
assume  x in A ; ::_thesis: x in bool (union A)
then  x c= union A by Lm15;
hence  x in bool (union A) by Def1; ::_thesis: verum
end;

theorem :: ZFMISC_1:83
for A, B being set st ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ) holds
union (A /\ B) = (union A) /\ (union B)
proof
let A, B be set ; ::_thesis: ( ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ) implies union (A /\ B) = (union A) /\ (union B) )
assume A1: for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ; ::_thesis: union (A /\ B) = (union A) /\ (union B)
A2: (union A) /\ (union B) c= union (A /\ B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union A) /\ (union B) or x in union (A /\ B) )
assume A3: x in (union A) /\ (union B) ; ::_thesis: x in union (A /\ B)
then  x in union A by XBOOLE_0:def_4;
then consider X being set  such that
A4: x in X and
A5: X in A by TARSKI:def_4;
 x in union B by A3, XBOOLE_0:def_4;
then consider Y being set  such that
A6: x in Y and
A7: Y in B by TARSKI:def_4;
now__::_thesis:_not_X_<>_Y
B8: x in X /\ Y by A4, A6, XBOOLE_0:def_4;
assume A9: X <> Y ; ::_thesis: contradiction
 ( X in A \/ B & Y in A \/ B ) by A5, A7, XBOOLE_0:def_3;
hence  contradiction by A1, A9, B8, XBOOLE_0:4; ::_thesis: verum
end;
then  Y in A /\ B by A5, A7, XBOOLE_0:def_4;
hence  x in union (A /\ B) by A6, TARSKI:def_4; ::_thesis: verum
end;
 union (A /\ B) c= (union A) /\ (union B) by Th79;
hence  union (A /\ B) = (union A) /\ (union B) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th84: :: ZFMISC_1:84
for A, X, Y, z being set st A c= [:X,Y:] & z in A holds
ex x, y being set st
( x in X & y in Y & z = [x,y] )
proof
let A, X, Y, z be set ; ::_thesis: ( A c= [:X,Y:] & z in A implies ex x, y being set st
( x in X & y in Y & z = [x,y] ) )
assume  ( A c= [:X,Y:] & z in A ) ; ::_thesis: ex x, y being set st
( x in X & y in Y & z = [x,y] )
then  z in [:X,Y:] by TARSKI:def_3;
hence  ex x, y being set st
( x in X & y in Y & z = [x,y] ) by Def2; ::_thesis: verum
end;

theorem Th85: :: ZFMISC_1:85
for z, X1, Y1, X2, Y2 being set st z in [:X1,Y1:] /\ [:X2,Y2:] holds
ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )
proof
let z, X1, Y1, X2, Y2 be set ; ::_thesis: ( z in [:X1,Y1:] /\ [:X2,Y2:] implies ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) )
assume A1: z in [:X1,Y1:] /\ [:X2,Y2:] ; ::_thesis: ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )
then  z in [:X1,Y1:] by XBOOLE_0:def_4;
then consider x1, y1 being set  such that
A2: x1 in X1 and
A3: y1 in Y1 and
A4: z = [x1,y1] by Def2;
 z in [:X2,Y2:] by A1, XBOOLE_0:def_4;
then consider x2, y2 being set  such that
A5: x2 in X2 and
A6: y2 in Y2 and
A7: z = [x2,y2] by Def2;
 y1 = y2 by A4, A7, XTUPLE_0:1;
then A8: y1 in Y1 /\ Y2 by A3, A6, XBOOLE_0:def_4;
 x1 = x2 by A4, A7, XTUPLE_0:1;
then  x1 in X1 /\ X2 by A2, A5, XBOOLE_0:def_4;
hence  ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by A4, A8; ::_thesis: verum
end;

theorem :: ZFMISC_1:86
for X, Y being set holds [:X,Y:] c= bool (bool (X \/ Y))
proof
let X, Y be set ; ::_thesis: [:X,Y:] c= bool (bool (X \/ Y))
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:X,Y:] or z in bool (bool (X \/ Y)) )
assume  z in [:X,Y:] ; ::_thesis: z in bool (bool (X \/ Y))
then consider x, y being set  such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by Def2;
 z c= bool (X \/ Y)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in z or u in bool (X \/ Y) )
assume  u in z ; ::_thesis: u in bool (X \/ Y)
then A4: ( u = {x,y} or u = {x} ) by A3, TARSKI:def_2;
 ( X c= X \/ Y & {x} c= X ) by A1, Lm1, XBOOLE_1:7;
then A5: {x} c= X \/ Y by XBOOLE_1:1;
 ( x in X \/ Y & y in X \/ Y ) by A1, A2, XBOOLE_0:def_3;
then  {x,y} c= X \/ Y by Th32;
hence  u in bool (X \/ Y) by A5, A4, Def1; ::_thesis: verum
end;
hence  z in bool (bool (X \/ Y)) by Def1; ::_thesis: verum
end;

theorem :: ZFMISC_1:87
for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) ) by Lm17;

theorem Th88: :: ZFMISC_1:88
for x, y, X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]
proof
let x, y, X, Y be set ; ::_thesis: ( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] )
 ( [x,y] in [:X,Y:] implies ( x in X & y in Y ) ) by Lm17;
hence  ( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] ) by Lm17; ::_thesis: verum
end;

theorem :: ZFMISC_1:89
for X1, Y1, X2, Y2 being set st ( for x, y being set holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) holds
[:X1,Y1:] = [:X2,Y2:]
proof
let X1, Y1, X2, Y2 be set ; ::_thesis: ( ( for x, y being set holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) implies [:X1,Y1:] = [:X2,Y2:] )
assume A1: for x, y being set holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ; ::_thesis: [:X1,Y1:] = [:X2,Y2:]
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_[:X1,Y1:]_implies_z_in_[:X2,Y2:]_)_&_(_z_in_[:X2,Y2:]_implies_z_in_[:X1,Y1:]_)_)
let z be set ; ::_thesis: ( ( z in [:X1,Y1:] implies z in [:X2,Y2:] ) & ( z in [:X2,Y2:] implies z in [:X1,Y1:] ) )
thus  ( z in [:X1,Y1:] implies z in [:X2,Y2:] ) ::_thesis: ( z in [:X2,Y2:] implies z in [:X1,Y1:] )
proof
assume A2: z in [:X1,Y1:] ; ::_thesis: z in [:X2,Y2:]
then  ex x, y being set st
( x in X1 & y in Y1 & [x,y] = z ) by Def2;
hence  z in [:X2,Y2:] by A1, A2; ::_thesis: verum
end;
assume A3: z in [:X2,Y2:] ; ::_thesis: z in [:X1,Y1:]
then  ex x, y being set st
( x in X2 & y in Y2 & [x,y] = z ) by Def2;
hence  z in [:X1,Y1:] by A1, A3; ::_thesis: verum
end;
hence  [:X1,Y1:] = [:X2,Y2:] by TARSKI:1; ::_thesis: verum
end;

Lm18:  for A, X1, Y1, B, X2, Y2 being set st A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
proof
let A, X1, Y1, B, X2, Y2 be set ; ::_thesis: ( A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) implies A = B )
assume that
A1: A c= [:X1,Y1:] and
A2: B c= [:X2,Y2:] and
A3: for x, y being set holds
( [x,y] in A iff [x,y] in B ) ; ::_thesis: A = B
now__::_thesis:_for_z_being_set_holds_
(_z_in_A_iff_z_in_B_)
let z be set ; ::_thesis: ( z in A iff z in B )
A4: ( z in B implies ex x, y being set st
( x in X2 & y in Y2 & z = [x,y] ) ) by A2, Th84;
 ( z in A implies ex x, y being set st
( x in X1 & y in Y1 & z = [x,y] ) ) by A1, Th84;
hence  ( z in A iff z in B ) by A3, A4; ::_thesis: verum
end;
hence  A = B by TARSKI:1; ::_thesis: verum
end;

Lm19:  for A, B being set st ( for z being set st z in A holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
proof
let A, B be set ; ::_thesis: ( ( for z being set st z in A holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) implies A = B )
assume that
A1: for z being set st z in A holds
ex x, y being set st z = [x,y] and
A2: for z being set st z in B holds
ex x, y being set st z = [x,y] and
A3: for x, y being set holds
( [x,y] in A iff [x,y] in B ) ; ::_thesis: A = B
now__::_thesis:_for_z_being_set_holds_
(_z_in_A_iff_z_in_B_)
let z be set ; ::_thesis: ( z in A iff z in B )
A4: ( z in B implies ex x, y being set st z = [x,y] ) by A2;
 ( z in A implies ex x, y being set st z = [x,y] ) by A1;
hence  ( z in A iff z in B ) by A3, A4; ::_thesis: verum
end;
hence  A = B by TARSKI:1; ::_thesis: verum
end;

theorem Th90: :: ZFMISC_1:90
for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )
proof
let X, Y be set ; ::_thesis: ( [:X,Y:] = {} iff ( X = {} or Y = {} ) )
thus  ( not [:X,Y:] = {} or X = {} or Y = {} ) ::_thesis: ( ( X = {} or Y = {} ) implies [:X,Y:] = {} )
proof
assume A1: [:X,Y:] = {} ; ::_thesis: ( X = {} or Y = {} )
assume  X <> {} ; ::_thesis: Y = {}
then consider x being set  such that
A2: x in X by XBOOLE_0:7;
assume  Y <> {} ; ::_thesis: contradiction
then consider y being set  such that
A3: y in Y by XBOOLE_0:7;
 [x,y] in [:X,Y:] by A2, A3, Def2;
hence  contradiction by A1; ::_thesis: verum
end;
assume A4: ( ( X = {} or Y = {} ) & not [:X,Y:] = {} ) ; ::_thesis: contradiction
then consider z being set  such that
A5: z in [:X,Y:] by XBOOLE_0:7;
A6: now__::_thesis:_not_Y_=_{}
assume A7: Y = {} ; ::_thesis: contradiction
 ex x, y being set st
( x in X & y in Y & [x,y] = z ) by A5, Def2;
hence  contradiction by A7; ::_thesis: verum
end;
now__::_thesis:_not_X_=_{}
assume A8: X = {} ; ::_thesis: contradiction
 ex x, y being set st
( x in X & y in Y & [x,y] = z ) by A5, Def2;
hence  contradiction by A8; ::_thesis: verum
end;
hence  contradiction by A4, A6; ::_thesis: verum
end;

theorem :: ZFMISC_1:91
for X, Y being set st X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] holds
X = Y
proof
let X, Y be set ; ::_thesis: ( X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y )
assume  X <> {} ; ::_thesis: ( not Y <> {} or not [:X,Y:] = [:Y,X:] or X = Y )
then consider x being set  such that
A1: x in X by XBOOLE_0:7;
assume  Y <> {} ; ::_thesis: ( not [:X,Y:] = [:Y,X:] or X = Y )
then consider y being set  such that
A2: y in Y by XBOOLE_0:7;
assume A3: [:X,Y:] = [:Y,X:] ; ::_thesis: X = Y
 for z being set holds
( z in X iff z in Y )
proof
let z be set ; ::_thesis: ( z in X iff z in Y )
thus  ( z in X implies z in Y ) ::_thesis: ( z in Y implies z in X )
proof
assume  z in X ; ::_thesis: z in Y
then  [z,y] in [:Y,X:] by A2, A3, Lm17;
hence  z in Y by Lm17; ::_thesis: verum
end;
assume  z in Y ; ::_thesis: z in X
then  [z,x] in [:X,Y:] by A1, A3, Lm17;
hence  z in X by Lm17; ::_thesis: verum
end;
hence  X = Y by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:92
for X, Y being set st [:X,X:] = [:Y,Y:] holds
X = Y
proof
let X, Y be set ; ::_thesis: ( [:X,X:] = [:Y,Y:] implies X = Y )
assume A1: [:X,X:] = [:Y,Y:] ; ::_thesis: X = Y
 for x being set holds
( x in X iff x in Y )
proof
let x be set ; ::_thesis: ( x in X iff x in Y )
 ( x in X iff [x,x] in [:X,X:] ) by Lm17;
hence  ( x in X iff x in Y ) by A1, Lm17; ::_thesis: verum
end;
hence  X = Y by TARSKI:1; ::_thesis: verum
end;

Lm20:  for z, X, Y being set st z in [:X,Y:] holds
ex x, y being set st [x,y] = z
proof
let z, X, Y be set ; ::_thesis: ( z in [:X,Y:] implies ex x, y being set st [x,y] = z )
assume  z in [:X,Y:] ; ::_thesis: ex x, y being set st [x,y] = z
then  ex x, y being set st
( x in X & y in Y & [x,y] = z ) by Def2;
hence  ex x, y being set st [x,y] = z ; ::_thesis: verum
end;

theorem :: ZFMISC_1:93
for X being set st X c= [:X,X:] holds
X = {}
proof
let X be set ; ::_thesis: ( X c= [:X,X:] implies X = {} )
assume A1: X c= [:X,X:] ; ::_thesis: X = {}
assume  X <> {} ; ::_thesis: contradiction
then consider z being set  such that
A2: z in X by XBOOLE_0:7;
consider Y being set  such that
A3: Y in X \/ (union X) and
A4: X \/ (union X) misses Y by XREGULAR:1, A2;
now__::_thesis:_not_Y_in_X
assume A5: Y in X ; ::_thesis: contradiction
then consider x, y being set  such that
A6: Y = [x,y] by Lm20, A1, TARSKI:def_3;
A7: {x} in Y by A6, TARSKI:def_2;
 Y c= union X by A5, Lm15;
then  {x} in union X by A7, TARSKI:def_3;
then  {x} in X \/ (union X) by XBOOLE_0:def_3;
hence  contradiction by A4, A7, XBOOLE_0:3; ::_thesis: verum
end;
then  Y in union X by A3, XBOOLE_0:def_3;
then consider Z being set  such that
A8: Y in Z and
A9: Z in X by TARSKI:def_4;
 Z in [:X,X:] by A1, A9, TARSKI:def_3;
then consider x, y being set  such that
A10: x in X and
 y in X and
A11: Z = [x,y] by Def2;
 ( Y = {x} or Y = {x,y} ) by A8, A11, TARSKI:def_2;
then A12: x in Y by TARSKI:def_1, TARSKI:def_2;
 x in X \/ (union X) by A10, XBOOLE_0:def_3;
hence  contradiction by A4, A12, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: ZFMISC_1:94
for Z, X, Y being set st Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) holds
X c= Y
proof
let Z, X, Y be set ; ::_thesis: ( Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) implies X c= Y )
assume  Z <> {} ; ::_thesis: ( ( not [:X,Z:] c= [:Y,Z:] & not [:Z,X:] c= [:Z,Y:] ) or X c= Y )
then consider z being set  such that
A1: z in Z by XBOOLE_0:7;
assume A2: ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,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 ; ::_thesis: x in Y
then  ( [x,z] in [:X,Z:] & [z,x] in [:Z,X:] ) by A1, Def2;
then  ( [x,z] in [:Y,Z:] or [z,x] in [:Z,Y:] ) by A2, TARSKI:def_3;
hence  x in Y by Lm17; ::_thesis: verum
end;

theorem Th95: :: ZFMISC_1:95
for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )
proof
let X, Y, Z be set ; ::_thesis: ( X c= Y implies ( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] ) )
assume A1: X c= Y ; ::_thesis: ( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )
thus  [:X,Z:] c= [:Y,Z:] ::_thesis: [:Z,X:] c= [:Z,Y:]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:X,Z:] or z in [:Y,Z:] )
assume  z in [:X,Z:] ; ::_thesis: z in [:Y,Z:]
then consider x, y being set  such that
A2: x in X and
A3: ( y in Z & z = [x,y] ) by Def2;
 x in Y by A1, A2, TARSKI:def_3;
hence  z in [:Y,Z:] by A3, Def2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:Z,X:] or z in [:Z,Y:] )
assume  z in [:Z,X:] ; ::_thesis: z in [:Z,Y:]
then consider y, x being set  such that
A4: y in Z and
A5: x in X and
A6: z = [y,x] by Def2;
 x in Y by A1, A5, TARSKI:def_3;
hence  z in [:Z,Y:] by A4, A6, Def2; ::_thesis: verum
end;

theorem Th96: :: ZFMISC_1:96
for X1, Y1, X2, Y2 being set st X1 c= Y1 & X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]
proof
let X1, Y1, X2, Y2 be set ; ::_thesis: ( X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:] )
assume  ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: [:X1,X2:] c= [:Y1,Y2:]
then  ( [:X1,X2:] c= [:Y1,X2:] & [:Y1,X2:] c= [:Y1,Y2:] ) by Th95;
hence  [:X1,X2:] c= [:Y1,Y2:] by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th97: :: ZFMISC_1:97
for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
proof
let X, Y, Z be set ; ::_thesis: ( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
A1: for z being set st z in [:(X \/ Y),Z:] holds
ex x, y being set st z = [x,y] by Lm20;
A2: for x, y being set holds
( [x,y] in [:(X \/ Y),Z:] iff [x,y] in [:X,Z:] \/ [:Y,Z:] )
proof
let x, y be set ; ::_thesis: ( [x,y] in [:(X \/ Y),Z:] iff [x,y] in [:X,Z:] \/ [:Y,Z:] )
thus  ( [x,y] in [:(X \/ Y),Z:] implies [x,y] in [:X,Z:] \/ [:Y,Z:] ) ::_thesis: ( [x,y] in [:X,Z:] \/ [:Y,Z:] implies [x,y] in [:(X \/ Y),Z:] )
proof
assume A3: [x,y] in [:(X \/ Y),Z:] ; ::_thesis: [x,y] in [:X,Z:] \/ [:Y,Z:]
then  x in X \/ Y by Lm17;
then A4: ( x in X or x in Y ) by XBOOLE_0:def_3;
 y in Z by A3, Lm17;
then  ( [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) by A4, Lm17;
hence  [x,y] in [:X,Z:] \/ [:Y,Z:] by XBOOLE_0:def_3; ::_thesis: verum
end;
assume  [x,y] in [:X,Z:] \/ [:Y,Z:] ; ::_thesis: [x,y] in [:(X \/ Y),Z:]
then  ( [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) by XBOOLE_0:def_3;
then A5: ( ( x in X & y in Z ) or ( x in Y & y in Z ) ) by Lm17;
then  x in X \/ Y by XBOOLE_0:def_3;
hence  [x,y] in [:(X \/ Y),Z:] by A5, Lm17; ::_thesis: verum
end;
A6: for z, X1, X2, Y1, Y2 being set st z in [:X1,X2:] \/ [:Y1,Y2:] holds
ex x, y being set st z = [x,y]
proof
let z, X1, X2, Y1, Y2 be set ; ::_thesis: ( z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x, y being set st z = [x,y] )
assume  z in [:X1,X2:] \/ [:Y1,Y2:] ; ::_thesis: ex x, y being set st z = [x,y]
then  ( z in [:X1,X2:] or z in [:Y1,Y2:] ) by XBOOLE_0:def_3;
hence  ex x, y being set st z = [x,y] by Lm20; ::_thesis: verum
end;
then  for z being set st z in [:X,Z:] \/ [:Y,Z:] holds
ex x, y being set st z = [x,y] ;
hence A7: [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] by A1, A2, Lm19; ::_thesis: [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:]
A8: for y, x being set holds
( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )
proof
let y, x be set ; ::_thesis: ( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] )
A9: ( ( ( not [x,y] in [:X,Z:] & not [x,y] in [:Y,Z:] ) or [y,x] in [:Z,X:] or [y,x] in [:Z,Y:] ) & ( ( not [y,x] in [:Z,X:] & not [y,x] in [:Z,Y:] ) or [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] ) ) by Th88;
 ( [y,x] in [:Z,(X \/ Y):] iff [x,y] in [:(X \/ Y),Z:] ) by Th88;
hence  ( [y,x] in [:Z,(X \/ Y):] iff [y,x] in [:Z,X:] \/ [:Z,Y:] ) by A7, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
A10: for z being set st z in [:Z,(X \/ Y):] holds
ex x, y being set st z = [x,y] by Lm20;
 for z being set st z in [:Z,X:] \/ [:Z,Y:] holds
ex x, y being set st z = [x,y] by A6;
hence  [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] by A10, A8, Lm19; ::_thesis: verum
end;

theorem :: ZFMISC_1:98
for X1, X2, Y1, Y2 being set holds [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]
thus [:(X1 \/ X2),(Y1 \/ Y2):] = [:X1,(Y1 \/ Y2):] \/ [:X2,(Y1 \/ Y2):] by Th97
.= ([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,(Y1 \/ Y2):] by Th97
.= ([:X1,Y1:] \/ [:X1,Y2:]) \/ ([:X2,Y1:] \/ [:X2,Y2:]) by Th97
.= (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:] by XBOOLE_1:4 ; ::_thesis: verum
end;

theorem :: ZFMISC_1:99
for X, Y, Z being set holds
( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
proof
let X, Y, Z be set ; ::_thesis: ( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
A1: for x, y being set holds
( [x,y] in [:(X /\ Y),Z:] iff [x,y] in [:X,Z:] /\ [:Y,Z:] )
proof
let x, y be set ; ::_thesis: ( [x,y] in [:(X /\ Y),Z:] iff [x,y] in [:X,Z:] /\ [:Y,Z:] )
thus  ( [x,y] in [:(X /\ Y),Z:] implies [x,y] in [:X,Z:] /\ [:Y,Z:] ) ::_thesis: ( [x,y] in [:X,Z:] /\ [:Y,Z:] implies [x,y] in [:(X /\ Y),Z:] )
proof
assume A2: [x,y] in [:(X /\ Y),Z:] ; ::_thesis: [x,y] in [:X,Z:] /\ [:Y,Z:]
then A3: x in X /\ Y by Lm17;
A4: y in Z by A2, Lm17;
 x in Y by A3, XBOOLE_0:def_4;
then A5: [x,y] in [:Y,Z:] by A4, Lm17;
 x in X by A3, XBOOLE_0:def_4;
then  [x,y] in [:X,Z:] by A4, Lm17;
hence  [x,y] in [:X,Z:] /\ [:Y,Z:] by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A6: [x,y] in [:X,Z:] /\ [:Y,Z:] ; ::_thesis: [x,y] in [:(X /\ Y),Z:]
then  [x,y] in [:Y,Z:] by XBOOLE_0:def_4;
then A7: x in Y by Lm17;
A8: [x,y] in [:X,Z:] by A6, XBOOLE_0:def_4;
then  x in X by Lm17;
then A9: x in X /\ Y by A7, XBOOLE_0:def_4;
 y in Z by A8, Lm17;
hence  [x,y] in [:(X /\ Y),Z:] by A9, Lm17; ::_thesis: verum
end;
 [:X,Z:] /\ [:Y,Z:] c= [:X,Z:] by XBOOLE_1:17;
hence A10: [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] by A1, Lm18; ::_thesis: [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:]
A11: for y, x being set holds
( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] )
proof
let y, x be set ; ::_thesis: ( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] )
A12: ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] iff ( [y,x] in [:Z,X:] & [y,x] in [:Z,Y:] ) ) by Th88;
 ( [y,x] in [:Z,(X /\ Y):] iff [x,y] in [:(X /\ Y),Z:] ) by Th88;
hence  ( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] ) by A10, A12, XBOOLE_0:def_4; ::_thesis: verum
end;
 [:Z,X:] /\ [:Z,Y:] c= [:Z,X:] by XBOOLE_1:17;
hence  [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] by A11, Lm18; ::_thesis: verum
end;

theorem Th100: :: ZFMISC_1:100
for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]
 ( Y1 /\ Y2 c= Y2 & X1 /\ X2 c= X2 ) by XBOOLE_1:17;
then A1: [:(X1 /\ X2),(Y1 /\ Y2):] c= [:X2,Y2:] by Th96;
A2: [:X1,Y1:] /\ [:X2,Y2:] c= [:(X1 /\ X2),(Y1 /\ Y2):]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:X1,Y1:] /\ [:X2,Y2:] or z in [:(X1 /\ X2),(Y1 /\ Y2):] )
assume  z in [:X1,Y1:] /\ [:X2,Y2:] ; ::_thesis: z in [:(X1 /\ X2),(Y1 /\ Y2):]
then  ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by Th85;
hence  z in [:(X1 /\ X2),(Y1 /\ Y2):] by Def2; ::_thesis: verum
end;
 ( Y1 /\ Y2 c= Y1 & X1 /\ X2 c= X1 ) by XBOOLE_1:17;
then  [:(X1 /\ X2),(Y1 /\ Y2):] c= [:X1,Y1:] by Th96;
then  [:(X1 /\ X2),(Y1 /\ Y2):] c= [:X1,Y1:] /\ [:X2,Y2:] by A1, XBOOLE_1:19;
hence  [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:] by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: ZFMISC_1:101
for A, X, B, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]
proof
let A, X, B, Y be set ; ::_thesis: ( A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:] )
assume that
A1: A c= X and
A2: B c= Y ; ::_thesis: [:A,Y:] /\ [:X,B:] = [:A,B:]
A3: [:A,Y:] /\ [:X,B:] = [:(A /\ X),(Y /\ B):] by Th100;
 A /\ X = A by A1, XBOOLE_1:28;
hence  [:A,Y:] /\ [:X,B:] = [:A,B:] by A2, A3, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th102: :: ZFMISC_1:102
for X, Y, Z being set holds
( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )
proof
let X, Y, Z be set ; ::_thesis: ( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )
A1: for x, y being set holds
( [x,y] in [:(X \ Y),Z:] iff [x,y] in [:X,Z:] \ [:Y,Z:] )
proof
let x, y be set ; ::_thesis: ( [x,y] in [:(X \ Y),Z:] iff [x,y] in [:X,Z:] \ [:Y,Z:] )
thus  ( [x,y] in [:(X \ Y),Z:] implies [x,y] in [:X,Z:] \ [:Y,Z:] ) ::_thesis: ( [x,y] in [:X,Z:] \ [:Y,Z:] implies [x,y] in [:(X \ Y),Z:] )
proof
assume A2: [x,y] in [:(X \ Y),Z:] ; ::_thesis: [x,y] in [:X,Z:] \ [:Y,Z:]
then A3: x in X \ Y by Lm17;
then A4: x in X by XBOOLE_0:def_5;
 not x in Y by A3, XBOOLE_0:def_5;
then A5: not [x,y] in [:Y,Z:] by Lm17;
 y in Z by A2, Lm17;
then  [x,y] in [:X,Z:] by A4, Lm17;
hence  [x,y] in [:X,Z:] \ [:Y,Z:] by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A6: [x,y] in [:X,Z:] \ [:Y,Z:] ; ::_thesis: [x,y] in [:(X \ Y),Z:]
then A7: [x,y] in [:X,Z:] by XBOOLE_0:def_5;
then A8: y in Z by Lm17;
 not [x,y] in [:Y,Z:] by A6, XBOOLE_0:def_5;
then A9: ( not x in Y or not y in Z ) by Lm17;
 x in X by A7, Lm17;
then  x in X \ Y by A7, A9, Lm17, XBOOLE_0:def_5;
hence  [x,y] in [:(X \ Y),Z:] by A8, Lm17; ::_thesis: verum
end;
 [:X,Z:] \ [:Y,Z:] c= [:X,Z:] by XBOOLE_1:36;
hence A10: [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] by A1, Lm18; ::_thesis: [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:]
A11: for y, x being set holds
( [y,x] in [:Z,(X \ Y):] iff [y,x] in [:Z,X:] \ [:Z,Y:] )
proof
let y, x be set ; ::_thesis: ( [y,x] in [:Z,(X \ Y):] iff [y,x] in [:Z,X:] \ [:Z,Y:] )
A12: ( [x,y] in [:X,Z:] & not [x,y] in [:Y,Z:] iff ( [y,x] in [:Z,X:] & not [y,x] in [:Z,Y:] ) ) by Th88;
 ( [y,x] in [:Z,(X \ Y):] iff [x,y] in [:(X \ Y),Z:] ) by Th88;
hence  ( [y,x] in [:Z,(X \ Y):] iff [y,x] in [:Z,X:] \ [:Z,Y:] ) by A10, A12, XBOOLE_0:def_5; ::_thesis: verum
end;
 [:Z,X:] \ [:Z,Y:] c= [:Z,X:] by XBOOLE_1:36;
hence  [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] by A11, Lm18; ::_thesis: verum
end;

theorem :: ZFMISC_1:103
for X1, X2, Y1, Y2 being set holds [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
A1: [:Y1,X2:] /\ [:X1,Y2:] = [:(Y1 /\ X1),(X2 /\ Y2):] by Th100;
 ( Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 ) by XBOOLE_1:17;
then A2: [:(Y1 /\ X1),(X2 /\ Y2):] c= [:Y1,Y2:] by Th96;
A3: [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] c= [:X1,X2:] \ [:Y1,Y2:]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
A4: now__::_thesis:_(_z_in_[:(X1_\_Y1),X2:]_&_z_in_[:(X1_\_Y1),X2:]_\/_[:X1,(X2_\_Y2):]_implies_z_in_[:X1,X2:]_\_[:Y1,Y2:]_)
assume  z in [:(X1 \ Y1),X2:] ; ::_thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
then consider x, y being set  such that
A5: x in X1 \ Y1 and
A6: y in X2 and
A7: z = [x,y] by Def2;
 not x in Y1 by A5, XBOOLE_0:def_5;
then A8: not z in [:Y1,Y2:] by A7, Lm17;
 x in X1 by A5, XBOOLE_0:def_5;
then  z in [:X1,X2:] by A6, A7, Lm17;
hence  ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] ) by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
A9: now__::_thesis:_(_z_in_[:X1,(X2_\_Y2):]_&_z_in_[:(X1_\_Y1),X2:]_\/_[:X1,(X2_\_Y2):]_implies_z_in_[:X1,X2:]_\_[:Y1,Y2:]_)
assume  z in [:X1,(X2 \ Y2):] ; ::_thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
then consider x, y being set  such that
A10: x in X1 and
A11: y in X2 \ Y2 and
A12: z = [x,y] by Def2;
 not y in Y2 by A11, XBOOLE_0:def_5;
then A13: not z in [:Y1,Y2:] by A12, Lm17;
 y in X2 by A11, XBOOLE_0:def_5;
then  z in [:X1,X2:] by A10, A12, Lm17;
hence  ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] ) by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
assume  z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] ; ::_thesis: z in [:X1,X2:] \ [:Y1,Y2:]
hence  z in [:X1,X2:] \ [:Y1,Y2:] by A4, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
 ( [:(X1 \ Y1),X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:X1,Y2:] ) by Th102;
then  [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:(Y1 /\ X1),(X2 /\ Y2):] by A1, XBOOLE_1:54;
then  [:X1,X2:] \ [:Y1,Y2:] c= [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A2, XBOOLE_1:34;
hence  [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th104: :: ZFMISC_1:104
for X1, X2, Y1, Y2 being set st ( X1 misses X2 or Y1 misses Y2 ) holds
[:X1,Y1:] misses [:X2,Y2:]
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: ( ( X1 misses X2 or Y1 misses Y2 ) implies [:X1,Y1:] misses [:X2,Y2:] )
assume A1: ( X1 misses X2 or Y1 misses Y2 ) ; ::_thesis: [:X1,Y1:] misses [:X2,Y2:]
assume  not [:X1,Y1:] misses [:X2,Y2:] ; ::_thesis: contradiction
then consider z being set  such that
A2: z in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:4;
 ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by A2, Th85;
hence  contradiction by A1, XBOOLE_0:4; ::_thesis: verum
end;

theorem :: ZFMISC_1:105
for x, y, z, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
proof
let x, y, z, Y be set ; ::_thesis: ( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
A1: ( x in {z} iff x = z ) by TARSKI:def_1;
hence  ( [x,y] in [:{z},Y:] implies ( x = z & y in Y ) ) by Lm17; ::_thesis: ( x = z & y in Y implies [x,y] in [:{z},Y:] )
thus  ( x = z & y in Y implies [x,y] in [:{z},Y:] ) by A1, Lm17; ::_thesis: verum
end;

theorem :: ZFMISC_1:106
for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
proof
let x, y, X, z be set ; ::_thesis: ( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
A1: ( y in {z} iff y = z ) by TARSKI:def_1;
hence  ( [x,y] in [:X,{z}:] implies ( x in X & y = z ) ) by Lm17; ::_thesis: ( x in X & y = z implies [x,y] in [:X,{z}:] )
thus  ( x in X & y = z implies [x,y] in [:X,{z}:] ) by A1, Lm17; ::_thesis: verum
end;

theorem :: ZFMISC_1:107
for X, x being set st X <> {} holds
( [:{x},X:] <> {} & [:X,{x}:] <> {} ) by Th90;

theorem :: ZFMISC_1:108
for x, y, X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
proof
let x, y, X, Y be set ; ::_thesis: ( x <> y implies ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) )
assume  x <> y ; ::_thesis: ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
then  {x} misses {y} by Th11;
hence  ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) by Th104; ::_thesis: verum
end;

theorem :: ZFMISC_1:109
for x, y, X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
proof
let x, y, X be set ; ::_thesis: ( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
 {x,y} = {x} \/ {y} by ENUMSET1:1;
hence  ( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] ) by Th97; ::_thesis: verum
end;

theorem Th110: :: ZFMISC_1:110
for X1, Y1, X2, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 & Y1 = Y2 )
proof
let X1, Y1, X2, Y2 be set ; ::_thesis: ( X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies ( X1 = X2 & Y1 = Y2 ) )
assume A1: X1 <> {} ; ::_thesis: ( not Y1 <> {} or not [:X1,Y1:] = [:X2,Y2:] or ( X1 = X2 & Y1 = Y2 ) )
then consider x being set  such that
A2: x in X1 by XBOOLE_0:7;
assume A3: Y1 <> {} ; ::_thesis: ( not [:X1,Y1:] = [:X2,Y2:] or ( X1 = X2 & Y1 = Y2 ) )
then consider y being set  such that
A4: y in Y1 by XBOOLE_0:7;
assume A5: [:X1,Y1:] = [:X2,Y2:] ; ::_thesis: ( X1 = X2 & Y1 = Y2 )
then A6: [:X2,Y2:] <> {} by A1, A3, Th90;
then A7: Y2 <> {} by Th90;
 for z being set holds
( z in X1 iff z in X2 )
proof
let z be set ; ::_thesis: ( z in X1 iff z in X2 )
consider y2 being set  such that
A8: y2 in Y2 by A7, XBOOLE_0:7;
thus  ( z in X1 implies z in X2 ) ::_thesis: ( z in X2 implies z in X1 )
proof
assume  z in X1 ; ::_thesis: z in X2
then  [z,y] in [:X2,Y2:] by A4, A5, Lm17;
hence  z in X2 by Lm17; ::_thesis: verum
end;
assume  z in X2 ; ::_thesis: z in X1
then  [z,y2] in [:X2,Y2:] by A8, Lm17;
hence  z in X1 by A5, Lm17; ::_thesis: verum
end;
hence  X1 = X2 by TARSKI:1; ::_thesis: Y1 = Y2
A9: X2 <> {} by A6, Th90;
 for z being set holds
( z in Y1 iff z in Y2 )
proof
let z be set ; ::_thesis: ( z in Y1 iff z in Y2 )
consider x2 being set  such that
A10: x2 in X2 by A9, XBOOLE_0:7;
thus  ( z in Y1 implies z in Y2 ) ::_thesis: ( z in Y2 implies z in Y1 )
proof
assume  z in Y1 ; ::_thesis: z in Y2
then  [x,z] in [:X2,Y2:] by A2, A5, Lm17;
hence  z in Y2 by Lm17; ::_thesis: verum
end;
assume  z in Y2 ; ::_thesis: z in Y1
then  [x2,z] in [:X2,Y2:] by A10, Lm17;
hence  z in Y1 by A5, Lm17; ::_thesis: verum
end;
hence  Y1 = Y2 by TARSKI:1; ::_thesis: verum
end;

theorem :: ZFMISC_1:111
for X, Y being set st ( X c= [:X,Y:] or X c= [:Y,X:] ) holds
X = {}
proof
let X, Y be set ; ::_thesis: ( ( X c= [:X,Y:] or X c= [:Y,X:] ) implies X = {} )
assume A1: ( X c= [:X,Y:] or X c= [:Y,X:] ) ; ::_thesis: X = {}
assume A2: X <> {} ; ::_thesis: contradiction
A3: now__::_thesis:_not_X_c=_[:Y,X:]
defpred S1[ set ] means  ex Y being set st
( $1 = Y & ex z being set st
( z in Y & z in X ) );
consider Z being set  such that
A4: for y being set holds
( y in Z iff ( y in union X & S1[y] ) ) from XBOOLE_0:sch_1();
consider Y2 being set  such that
A5: Y2 in X \/ Z and
A6: X \/ Z misses Y2 by XREGULAR:1, A2;
now__::_thesis:_ex_Y2_being_set_st_
(_Y2_in_X_&_(_for_Y1_being_set_st_Y1_in_Y2_holds_
for_z_being_set_holds_
(_not_z_in_Y1_or_not_z_in_X_)_)_)
assume A7: for Y2 being set holds
( not Y2 in X or ex Y1 being set st
( Y1 in Y2 & ex z being set st
( z in Y1 & z in X ) ) ) ; ::_thesis: contradiction
now__::_thesis:_not_Y2_in_X
assume A8: Y2 in X ; ::_thesis: contradiction
then consider Y1 being set  such that
A9: Y1 in Y2 and
A10: ex z being set st
( z in Y1 & z in X ) by A7;
 Y1 in union X by A8, A9, TARSKI:def_4;
then  Y1 in Z by A4, A10;
then  Y1 in X \/ Z by XBOOLE_0:def_3;
hence  contradiction by A6, A9, XBOOLE_0:3; ::_thesis: verum
end;
then  Y2 in Z by A5, XBOOLE_0:def_3;
then  ex X2 being set st
( Y2 = X2 & ex z being set st
( z in X2 & z in X ) ) by A4;
then consider z being set  such that
A11: z in Y2 and
A12: z in X ;
 z in X \/ Z by A12, XBOOLE_0:def_3;
hence  contradiction by A6, A11, XBOOLE_0:3; ::_thesis: verum
end;
then consider Y1 being set  such that
A13: Y1 in X and
A14: for Y2 being set holds
( not Y2 in Y1 or for z being set holds
( not z in Y2 or not z in X ) ) ;
A15: now__::_thesis:_for_y,_x_being_set_holds_
(_not_x_in_X_or_not_Y1_=_[y,x]_)
given y, x being set  such that A16: x in X and
A17: Y1 = [y,x] ; ::_thesis: contradiction
A18: x in {y,x} by TARSKI:def_2;
 {y,x} in Y1 by A17, TARSKI:def_2;
hence  contradiction by A14, A16, A18; ::_thesis: verum
end;
assume  X c= [:Y,X:] ; ::_thesis: contradiction
then  Y1 in [:Y,X:] by A13, TARSKI:def_3;
then  ex y, x being set st
( y in Y & x in X & Y1 = [y,x] ) by Def2;
hence  contradiction by A15; ::_thesis: verum
end;
now__::_thesis:_not_X_c=_[:X,Y:]
consider z being set  such that
A19: z in X by A2, XBOOLE_0:7;
consider Y1 being set  such that
A20: Y1 in X \/ (union X) and
A21: X \/ (union X) misses Y1 by XREGULAR:1, A19;
assume A22: X c= [:X,Y:] ; ::_thesis: contradiction
now__::_thesis:_not_Y1_in_X
assume A23: Y1 in X ; ::_thesis: contradiction
then consider x, y being set  such that
A24: Y1 = [x,y] by Lm20, A22, TARSKI:def_3;
A25: {x} in Y1 by A24, TARSKI:def_2;
 Y1 c= union X by A23, Lm15;
then  {x} in union X by A25, TARSKI:def_3;
then  {x} in X \/ (union X) by XBOOLE_0:def_3;
hence  contradiction by A21, A25, XBOOLE_0:3; ::_thesis: verum
end;
then  Y1 in union X by A20, XBOOLE_0:def_3;
then consider Y2 being set  such that
A26: Y1 in Y2 and
A27: Y2 in X by TARSKI:def_4;
 Y2 in [:X,Y:] by A22, A27, TARSKI:def_3;
then consider x, y being set  such that
A28: x in X and
 y in Y and
A29: Y2 = [x,y] by Def2;
 ( Y1 = {x} or Y1 = {x,y} ) by A26, A29, TARSKI:def_2;
then A30: x in Y1 by TARSKI:def_1, TARSKI:def_2;
 x in X \/ (union X) by A28, XBOOLE_0:def_3;
hence  contradiction by A21, A30, XBOOLE_0:3; ::_thesis: verum
end;
hence  contradiction by A1, A3; ::_thesis: verum
end;

theorem :: ZFMISC_1:112
for N being set ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
proof
let N be set ; ::_thesis: ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
consider M being set  such that
A1: N in M and
A2: for X, Y being set st X in M & Y c= X holds
Y in M and
A3: for X being set st X in M holds
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) and
A4: for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by TARSKI:3;
take  M ; ::_thesis: ( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus  N in M by A1; ::_thesis: ( ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus  for X, Y being set st X in M & Y c= X holds
Y in M by A2; ::_thesis: ( ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus  for X being set st X in M holds
bool X in M ::_thesis: for X being set holds
( not X c= M or X,M are_equipotent or X in M )
proof
let X be set ; ::_thesis: ( X in M implies bool X in M )
assume  X in M ; ::_thesis: bool X in M
then consider Z being set  such that
A5: Z in M and
A6: for Y being set st Y c= X holds
Y in Z by A3;
now__::_thesis:_for_Y_being_set_st_Y_in_bool_X_holds_
Y_in_Z
let Y be set ; ::_thesis: ( Y in bool X implies Y in Z )
assume  Y in bool X ; ::_thesis: Y in Z
then  Y c= X by Def1;
hence  Y in Z by A6; ::_thesis: verum
end;
hence  bool X in M by A2, A5, TARSKI:def_3; ::_thesis: verum
end;
thus  for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by A4; ::_thesis: verum
end;


theorem :: ZFMISC_1:113
for e, X1, Y1, X2, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]
proof
let e, X1, Y1, X2, Y2 be set ; ::_thesis: ( e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:(X1 /\ X2),(Y1 /\ Y2):] )
assume  ( e in [:X1,Y1:] & e in [:X2,Y2:] ) ; ::_thesis: e in [:(X1 /\ X2),(Y1 /\ Y2):]
then  e in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:def_4;
hence  e in [:(X1 /\ X2),(Y1 /\ Y2):] by Th100; ::_thesis: verum
end;

begin

theorem Th114: :: ZFMISC_1:114
for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} holds
( X1 c= Y1 & X2 c= Y2 )
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: ( [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies ( X1 c= Y1 & X2 c= Y2 ) )
assume that
A1: [:X1,X2:] c= [:Y1,Y2:] and
A2: [:X1,X2:] <> {} ; ::_thesis: ( X1 c= Y1 & X2 c= Y2 )
A3: [:X1,X2:] = [:X1,X2:] /\ [:Y1,Y2:] by A1, XBOOLE_1:28
.= [:(X1 /\ Y1),(X2 /\ Y2):] by Th100 ;
 ( X1 <> {} & X2 <> {} ) by A2, Th90;
then  ( X1 = X1 /\ Y1 & X2 = X2 /\ Y2 ) by A3, Th110;
hence  ( X1 c= Y1 & X2 c= Y2 ) by XBOOLE_1:17; ::_thesis: verum
end;

theorem :: ZFMISC_1:115
for A being non empty set
for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds
B c= D
proof
let A be non empty set ; ::_thesis: for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds
B c= D
let B, C, D be set ; ::_thesis: ( ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) implies B c= D )
assume A1: ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) ; ::_thesis: B c= D
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: B c= D
hence  B c= D by XBOOLE_1:2; ::_thesis: verum
end;
suppose B <> {} ; ::_thesis: B c= D
then  ( [:A,B:] <> {} & [:B,A:] <> {} ) by Th90;
hence  B c= D by A1, Th114; ::_thesis: verum
end;
end;
end;

theorem :: ZFMISC_1:116
for x, X being set st x in X holds
(X \ {x}) \/ {x} = X
proof
let x, X be set ; ::_thesis: ( x in X implies (X \ {x}) \/ {x} = X )
assume A1: x in X ; ::_thesis: (X \ {x}) \/ {x} = X
thus  (X \ {x}) \/ {x} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= (X \ {x}) \/ {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (X \ {x}) \/ {x} or y in X )
assume  y in (X \ {x}) \/ {x} ; ::_thesis: y in X
then  ( y in X \ {x} or y in {x} ) by XBOOLE_0:def_3;
hence  y in X by A1, Th56, TARSKI:def_1; ::_thesis: verum
end;
thus  X c= (X \ {x}) \/ {x} ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in (X \ {x}) \/ {x} )
assume  y in X ; ::_thesis: y in (X \ {x}) \/ {x}
then  ( y in {x} or y in X \ {x} ) by XBOOLE_0:def_5;
hence  y in (X \ {x}) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;

theorem :: ZFMISC_1:117
for x, X being set st not x in X holds
(X \/ {x}) \ {x} = X
proof
let x, X be set ; ::_thesis: ( not x in X implies (X \/ {x}) \ {x} = X )
A1: (X \/ {x}) \ {x} = X \ {x} by XBOOLE_1:40;
assume  not x in X ; ::_thesis: (X \/ {x}) \ {x} = X
hence  (X \/ {x}) \ {x} = X by A1, Th57; ::_thesis: verum
end;

theorem :: ZFMISC_1:118
for x, y, z, Z being set holds
( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )
proof
let x, y, z, Z be set ; ::_thesis: ( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )
hereby  ::_thesis: ( ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) implies Z c= {x,y,z} )
assume that
A1: Z c= {x,y,z} and
A2: Z <> {} and
A3: Z <> {x} and
A4: Z <> {y} and
A5: Z <> {z} and
A6: Z <> {x,y} and
A7: Z <> {y,z} and
A8: Z <> {x,z} ; ::_thesis: Z = {x,y,z}
 {x,y,z} c= Z
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y,z} or a in Z )
A9: now__::_thesis:_x_in_Z
{x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:2
.= {y,z} \ {x} by XBOOLE_1:40 ;
then A10: {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
assume  not x in Z ; ::_thesis: contradiction
then  Z c= {x,y,z} \ {x} by A1, Lm2;
hence  contradiction by A2, A4, A5, A7, Lm14, A10, XBOOLE_1:1; ::_thesis: verum
end;
A11: now__::_thesis:_y_in_Z
{x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:3
.= (({x} \/ {y}) \/ {z}) \ {y} by ENUMSET1:1
.= (({x} \/ {z}) \/ {y}) \ {y} by XBOOLE_1:4
.= ({x,z} \/ {y}) \ {y} by ENUMSET1:1
.= {x,z} \ {y} by XBOOLE_1:40 ;
then A12: {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
assume  not y in Z ; ::_thesis: contradiction
then  Z c= {x,y,z} \ {y} by A1, Lm2;
hence  contradiction by A2, A3, A5, A8, Lm14, A12, XBOOLE_1:1; ::_thesis: verum
end;
A13: now__::_thesis:_z_in_Z
{x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:3
.= {x,y} \ {z} by XBOOLE_1:40 ;
then A14: {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
assume  not z in Z ; ::_thesis: contradiction
then  Z c= {x,y,z} \ {z} by A1, Lm2;
hence  contradiction by A2, A3, A4, A6, Lm14, A14, XBOOLE_1:1; ::_thesis: verum
end;
assume  a in {x,y,z} ; ::_thesis: a in Z
hence  a in Z by A9, A11, A13, ENUMSET1:def_1; ::_thesis: verum
end;
hence  Z = {x,y,z} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A15: ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) ; ::_thesis: Z c= {x,y,z}
percases ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) by A15;
suppose Z = {} ; ::_thesis: Z c= {x,y,z}
hence  Z c= {x,y,z} by XBOOLE_1:2; ::_thesis: verum
end;
suppose Z = {x} ; ::_thesis: Z c= {x,y,z}
then  Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence  Z c= {x,y,z} by ENUMSET1:2; ::_thesis: verum
end;
supposeA16: Z = {y} ; ::_thesis: Z c= {x,y,z}
 {x,y} c= {x,y} \/ {z} by XBOOLE_1:7;
then A17: {x,y} c= {x,y,z} by ENUMSET1:3;
 Z c= {x,y} by A16, Th7;
hence  Z c= {x,y,z} by A17, XBOOLE_1:1; ::_thesis: verum
end;
suppose Z = {z} ; ::_thesis: Z c= {x,y,z}
then  Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence  Z c= {x,y,z} by ENUMSET1:3; ::_thesis: verum
end;
suppose Z = {x,y} ; ::_thesis: Z c= {x,y,z}
then  Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence  Z c= {x,y,z} by ENUMSET1:3; ::_thesis: verum
end;
suppose Z = {y,z} ; ::_thesis: Z c= {x,y,z}
then  Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence  Z c= {x,y,z} by ENUMSET1:2; ::_thesis: verum
end;
supposeA18: Z = {x,z} ; ::_thesis: Z c= {x,y,z}
A19: {x,z} \/ {y} = ({x} \/ {z}) \/ {y} by ENUMSET1:1
.= {x} \/ ({y} \/ {z}) by XBOOLE_1:4
.= {x} \/ {y,z} by ENUMSET1:1 ;
 Z c= {x,z} \/ {y} by A18, XBOOLE_1:7;
hence  Z c= {x,y,z} by A19, ENUMSET1:2; ::_thesis: verum
end;
suppose Z = {x,y,z} ; ::_thesis: Z c= {x,y,z}
hence  Z c= {x,y,z} ; ::_thesis: verum
end;
end;
end;

theorem :: ZFMISC_1:119
for N, M, X1, Y1, X2, Y2 being set st N c= [:X1,Y1:] & M c= [:X2,Y2:] holds
N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]
proof
let N, M, X1, Y1, X2, Y2 be set ; ::_thesis: ( N c= [:X1,Y1:] & M c= [:X2,Y2:] implies N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):] )
assume  ( N c= [:X1,Y1:] & M c= [:X2,Y2:] ) ; ::_thesis: N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]
then A1: N \/ M c= [:X1,Y1:] \/ [:X2,Y2:] by XBOOLE_1:13;
 ( X1 c= X1 \/ X2 & Y1 c= Y1 \/ Y2 ) by XBOOLE_1:7;
then A2: [:X1,Y1:] c= [:(X1 \/ X2),(Y1 \/ Y2):] by Th96;
 ( Y2 c= Y1 \/ Y2 & X2 c= X1 \/ X2 ) by XBOOLE_1:7;
then  [:X2,Y2:] c= [:(X1 \/ X2),(Y1 \/ Y2):] by Th96;
then  [:X1,Y1:] \/ [:X2,Y2:] c= [:(X1 \/ X2),(Y1 \/ Y2):] by A2, XBOOLE_1:8;
hence  N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):] by A1, XBOOLE_1:1; ::_thesis: verum
end;

Lm21:  for x, y, X being set st not x in X & not y in X holds
{x,y} misses X
proof
let x, y, X be set ; ::_thesis: ( not x in X & not y in X implies {x,y} misses X )
assume A1: ( not x in X & not y in X ) ; ::_thesis: {x,y} misses X
thus  {x,y} /\ X c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= {x,y} /\ X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} /\ X or z in {} )
assume  z in {x,y} /\ X ; ::_thesis: z in {}
then  ( z in {x,y} & z in X ) by XBOOLE_0:def_4;
hence  z in {} by A1, TARSKI:def_2; ::_thesis: verum
end;
thus  {} c= {x,y} /\ X by XBOOLE_1:2; ::_thesis: verum
end;

theorem Th120: :: ZFMISC_1:120
for x, y, X being set st not x in X & not y in X holds
X = X \ {x,y}
proof
let x, y, X be set ; ::_thesis: ( not x in X & not y in X implies X = X \ {x,y} )
 ( X \ {x,y} = X iff X misses {x,y} ) by XBOOLE_1:83;
hence  ( not x in X & not y in X implies X = X \ {x,y} ) by Lm21; ::_thesis: verum
end;

theorem :: ZFMISC_1:121
for x, y, X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}
proof
let x, y, X be set ; ::_thesis: ( not x in X & not y in X implies X = (X \/ {x,y}) \ {x,y} )
A1: (X \/ {x,y}) \ {x,y} = X \ {x,y} by XBOOLE_1:40;
assume  ( not x in X & not y in X ) ; ::_thesis: X = (X \/ {x,y}) \ {x,y}
hence  X = (X \/ {x,y}) \ {x,y} by A1, Th120; ::_thesis: verum
end;

definition
let x1, x2, x3 be set ;
predx1,x2,x3 are_mutually_different  means :: ZFMISC_1:def 5
( x1 <> x2 & x1 <> x3 & x2 <> x3 );
end;

:: deftheorem  defines are_mutually_different ZFMISC_1:def_5_:_
 for x1, x2, x3 being set holds
( x1,x2,x3 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) );

definition
let x1, x2, x3, x4 be set ;
predx1,x2,x3,x4 are_mutually_different  means :: ZFMISC_1:def 6
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );
end;

:: deftheorem  defines are_mutually_different ZFMISC_1:def_6_:_
 for x1, x2, x3, x4 being set holds
( x1,x2,x3,x4 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) );

definition
let x1, x2, x3, x4, x5 be set ;
predx1,x2,x3,x4,x5 are_mutually_different  means :: ZFMISC_1:def 7
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 );
end;

:: deftheorem  defines are_mutually_different ZFMISC_1:def_7_:_
 for x1, x2, x3, x4, x5 being set holds
( x1,x2,x3,x4,x5 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 ) );

definition
let x1, x2, x3, x4, x5, x6 be set ;
predx1,x2,x3,x4,x5,x6 are_mutually_different  means :: ZFMISC_1:def 8
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 );
end;

:: deftheorem  defines are_mutually_different ZFMISC_1:def_8_:_
 for x1, x2, x3, x4, x5, x6 being set holds
( x1,x2,x3,x4,x5,x6 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 ) );

definition
let x1, x2, x3, x4, x5, x6, x7 be set ;
predx1,x2,x3,x4,x5,x6,x7 are_mutually_different  means :: ZFMISC_1:def 9
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 );
end;

:: deftheorem  defines are_mutually_different ZFMISC_1:def_9_:_
 for x1, x2, x3, x4, x5, x6, x7 being set holds
( x1,x2,x3,x4,x5,x6,x7 are_mutually_different iff ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 ) );

theorem :: ZFMISC_1:122
for x1, x2, y1, y2 being set holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
let x1, x2, y1, y2 be set ; ::_thesis: [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
thus [:{x1,x2},{y1,y2}:] = [:({x1} \/ {x2}),{y1,y2}:] by ENUMSET1:1
.= [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by Th97
.= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by Th30
.= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by Th30
.= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5 ; ::_thesis: verum
end;

theorem :: ZFMISC_1:123
for x, y, A being set st x <> y holds
(A \/ {x}) \ {y} = (A \ {y}) \/ {x} by Th11, XBOOLE_1:87;

definition
let X be set ;
attrX is trivial  means :Def10: :: ZFMISC_1:def 10
 for x, y being set st x in X & y in X holds
x = y;
end;

:: deftheorem Def10 defines trivial ZFMISC_1:def_10_:_
 for X being set holds
( X is trivial iff for x, y being set st x in X & y in X holds
x = y );

registration
cluster empty  ->  trivial for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is trivial
proof
let X be set ; ::_thesis: ( X is empty implies X is trivial )
assume A1: X is empty ; ::_thesis: X is trivial
let x be set ; :: according to ZFMISC_1:def_10 ::_thesis: for y being set st x in X & y in X holds
x = y
let y be set ; ::_thesis: ( x in X & y in X implies x = y )
thus  ( x in X & y in X implies x = y ) by A1; ::_thesis: verum
end;
end;

registration
cluster non trivial  ->  non empty for set ;
coherence
 for b1 being set st not b1 is trivial holds
not b1 is empty ;
end;

registration
let x be set ;
cluster{x} ->  trivial ;
coherence
 {x} is trivial
proof
let y be set ; :: according to ZFMISC_1:def_10 ::_thesis: for y being set st y in {x} & y in {x} holds
y = y
let z be set ; ::_thesis: ( y in {x} & z in {x} implies y = z )
assume that
A1: y in {x} and
A2: z in {x} ; ::_thesis: y = z
 y = x by A1, TARSKI:def_1;
hence  y = z by A2, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty trivial for set ;
existence
 ex b1 being set st
( b1 is trivial & not b1 is empty )
proof
take  {{}} ; ::_thesis: ( {{}} is trivial & not {{}} is empty )
thus  ( {{}} is trivial & not {{}} is empty ) ; ::_thesis: verum
end;
end;

theorem :: ZFMISC_1:124
for A, B, C, p being set st A c= B & B /\ C = {p} & p in A holds
A /\ C = {p}
proof
let A, B, C, p be set ; ::_thesis: ( A c= B & B /\ C = {p} & p in A implies A /\ C = {p} )
assume A1: A c= B ; ::_thesis: ( not B /\ C = {p} or not p in A or A /\ C = {p} )
assume A2: B /\ C = {p} ; ::_thesis: ( not p in A or A /\ C = {p} )
 p in B /\ C by A2, TARSKI:def_1;
then A4: p in C by XBOOLE_0:def_4;
assume  p in A ; ::_thesis: A /\ C = {p}
then  p in A /\ C by A4, XBOOLE_0:def_4;
hence  A /\ C = {p} by A2, Lm3, A1, XBOOLE_1:26; ::_thesis: verum
end;

theorem :: ZFMISC_1:125
for A, B, C, p being set st A /\ B c= {p} & p in C & C misses B holds
A \/ C misses B
proof
let A, B, C, p be set ; ::_thesis: ( A /\ B c= {p} & p in C & C misses B implies A \/ C misses B )
assume that
A1: A /\ B c= {p} and
A2: p in C and
A3: C misses B ; ::_thesis: A \/ C misses B
 {p} c= C by A2, Lm1;
then  A /\ B c= C by A1, XBOOLE_1:1;
then  (A /\ B) /\ B c= C /\ B by XBOOLE_1:27;
then A4: A /\ (B /\ B) c= C /\ B by XBOOLE_1:16;
(A \/ C) /\ B = (A /\ B) \/ (C /\ B) by XBOOLE_1:23
.= C /\ B by A4, XBOOLE_1:12
.= {} by A3, XBOOLE_0:def_7 ;
hence  A \/ C misses B by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: ZFMISC_1:126
for A, B being set st ( for x, y being set st x in A & y in B holds
x misses y ) holds
union A misses union B
proof
let A, B be set ; ::_thesis: ( ( for x, y being set st x in A & y in B holds
x misses y ) implies union A misses union B )
assume A1: for x, y being set st x in A & y in B holds
x misses y ; ::_thesis: union A misses union B
 for y being set st y in B holds
union A misses y
proof
let y be set ; ::_thesis: ( y in B implies union A misses y )
assume  y in B ; ::_thesis: union A misses y
then  for x being set st x in A holds
x misses y by A1;
hence  union A misses y by Th80; ::_thesis: verum
end;
hence  union A misses union B by Th80; ::_thesis: verum
end;

registration
let X be set ;
let Y be empty set ;
cluster[:X,Y:] ->  empty ;
coherence
 [:X,Y:] is empty by Th90;
end;

registration
let X be empty set ;
let Y be set ;
cluster[:X,Y:] ->  empty ;
coherence
 [:X,Y:] is empty by Th90;
end;

theorem :: ZFMISC_1:127
for A, B being set holds not A in [:A,B:]
proof
let A, B be set ; ::_thesis: not A in [:A,B:]
assume  A in [:A,B:] ; ::_thesis: contradiction
then consider x, y being set  such that
A1: ( x in A & y in B & A = [x,y] ) by Th84;
 ( x = {x} or x = {x,y} ) by A1, TARSKI:def_2;
then  x in x by TARSKI:def_1, TARSKI:def_2;
hence  contradiction ; ::_thesis: verum
end;

theorem :: ZFMISC_1:128
for x being set holds [x,{x}] in [:{x},[x,{x}]:]
proof
let x be set ; ::_thesis: [x,{x}] in [:{x},[x,{x}]:]
 [:{x},[x,{x}]:] = {[x,{x}],[x,{x,{x}}]} by Th30;
hence  [x,{x}] in [:{x},[x,{x}]:] by TARSKI:def_2; ::_thesis: verum
end;

theorem :: ZFMISC_1:129
for B, A being set st B in [:A,B:] holds
ex x being set st
( x in A & B = [x,{x}] )
proof
let B, A be set ; ::_thesis: ( B in [:A,B:] implies ex x being set st
( x in A & B = [x,{x}] ) )
assume  B in [:A,B:] ; ::_thesis: ex x being set st
( x in A & B = [x,{x}] )
then consider x, y being set  such that
A1: ( x in A & y in B & B = [x,y] ) by Th84;
take  x ; ::_thesis: ( x in A & B = [x,{x}] )
thus  x in A by A1; ::_thesis: B = [x,{x}]
percases ( y = {x} or y = {x,y} ) by A1, TARSKI:def_2;
suppose y = {x} ; ::_thesis: B = [x,{x}]
hence  B = [x,{x}] by A1; ::_thesis: verum
end;
suppose y = {x,y} ; ::_thesis: B = [x,{x}]
then  y in y by TARSKI:def_2;
hence  B = [x,{x}] ; ::_thesis: verum
end;
end;
end;

theorem :: ZFMISC_1:130
for B, A being set st B c= A & A is trivial holds
B is trivial
proof
let B, A be set ; ::_thesis: ( B c= A & A is trivial implies B is trivial )
assume that
A1: B c= A and
A2: A is trivial ; ::_thesis: B is trivial
let x be set ; :: according to ZFMISC_1:def_10 ::_thesis: for y being set st x in B & y in B holds
x = y
let y be set ; ::_thesis: ( x in B & y in B implies x = y )
assume  ( x in B & y in B ) ; ::_thesis: x = y
then  ( x in A & y in A ) by A1, TARSKI:def_3;
hence  x = y by A2, Def10; ::_thesis: verum
end;

registration
cluster non trivial for set ;
existence
 not for b1 being set holds b1 is trivial
proof
take  {{},{{}}} ; ::_thesis: not {{},{{}}} is trivial
take  {} ; :: according to ZFMISC_1:def_10 ::_thesis: ex y being set st
( {} in {{},{{}}} & y in {{},{{}}} & not {} = y )
take  {{}} ; ::_thesis: ( {} in {{},{{}}} & {{}} in {{},{{}}} & not {} = {{}} )
thus  ( {} in {{},{{}}} & {{}} in {{},{{}}} ) by TARSKI:def_2; ::_thesis: not {} = {{}}
thus  {} <> {{}} ; ::_thesis: verum
end;
end;

theorem Th131: :: ZFMISC_1:131
for X being set st not X is empty & X is trivial holds
ex x being set st X = {x}
proof
let X be set ; ::_thesis: ( not X is empty & X is trivial implies ex x being set st X = {x} )
assume  not X is empty ; ::_thesis: ( not X is trivial or ex x being set st X = {x} )
then consider x being set  such that
A1: x in X by XBOOLE_0:def_1;
assume A2: X is trivial ; ::_thesis: ex x being set st X = {x}
take  x ; ::_thesis: X = {x}
 for y being set holds
( y in X iff x = y ) by A2, A1, Def10;
hence  X = {x} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:132
for x being set
for X being trivial set st x in X holds
X = {x}
proof
let x be set ; ::_thesis: for X being trivial set st x in X holds
X = {x}
let X be trivial set ; ::_thesis: ( x in X implies X = {x} )
assume A1: x in X ; ::_thesis: X = {x}
then  ex x being set st X = {x} by Th131;
hence  X = {x} by A1, TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:133
for a, b, c, X being set st a in X & b in X & c in X holds
{a,b,c} c= X
proof
let a, b, c, X be set ; ::_thesis: ( a in X & b in X & c in X implies {a,b,c} c= X )
assume  ( a in X & b in X & c in X ) ; ::_thesis: {a,b,c} c= X
then  ( {a,b} c= X & {c} c= X ) by Lm1, Th32;
then  {a,b} \/ {c} c= X by XBOOLE_1:8;
hence  {a,b,c} c= X by ENUMSET1:3; ::_thesis: verum
end;

theorem :: ZFMISC_1:134
for x, y, X being set st [x,y] in X holds
( x in union (union X) & y in union (union X) )
proof
let x, y, X be set ; ::_thesis: ( [x,y] in X implies ( x in union (union X) & y in union (union X) ) )
assume A1: [x,y] in X ; ::_thesis: ( x in union (union X) & y in union (union X) )
 {x} in [x,y] by TARSKI:def_2;
then A2: {x} in union X by A1, TARSKI:def_4;
 {x,y} in [x,y] by TARSKI:def_2;
then A3: {x,y} in union X by A1, TARSKI:def_4;
 ( y in {x,y} & x in {x} ) by TARSKI:def_1, TARSKI:def_2;
hence  ( x in union (union X) & y in union (union X) ) by A3, A2, TARSKI:def_4; ::_thesis: verum
end;

theorem Th135: :: ZFMISC_1:135
for Y, x, X being set holds
( not X c= Y \/ {x} or x in X or X c= Y )
proof
let Y, x, X be set ; ::_thesis: ( not X c= Y \/ {x} or x in X or X c= Y )
assume that
A1: X c= Y \/ {x} and
A2: not x in X ; ::_thesis: X c= Y
X = X /\ (Y \/ {x}) by A1, XBOOLE_1:28
.= (X /\ Y) \/ (X /\ {x}) by XBOOLE_1:23
.= (X /\ Y) \/ {} by A2, Lm7, XBOOLE_0:def_7
.= X /\ Y ;
hence  X c= Y by XBOOLE_1:17; ::_thesis: verum
end;

theorem :: ZFMISC_1:136
for x, y, X being set holds
( x in X \/ {y} iff ( x in X or x = y ) )
proof
let x, y, X be set ; ::_thesis: ( x in X \/ {y} iff ( x in X or x = y ) )
 ( x in X \/ {y} iff ( x in X or x in {y} ) ) by XBOOLE_0:def_3;
hence  ( x in X \/ {y} iff ( x in X or x = y ) ) by TARSKI:def_1; ::_thesis: verum
end;

theorem :: ZFMISC_1:137
for x, Y, X being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
proof
let x, Y, X be set ; ::_thesis: ( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
 ( X c= Y & {x} c= Y implies X \/ {x} c= Y ) by XBOOLE_1:8;
hence  ( X \/ {x} c= Y iff ( x in Y & X c= Y ) ) by Lm1, XBOOLE_1:11; ::_thesis: verum
end;

theorem :: ZFMISC_1:138
for A, B, a being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B
proof
let A, B, a be set ; ::_thesis: ( A c= B & B c= A \/ {a} & not A \/ {a} = B implies A = B )
assume that
A1: A c= B and
A2: B c= A \/ {a} ; ::_thesis: ( A \/ {a} = B or A = B )
assume that
A3: A \/ {a} <> B and
A4: A <> B ; ::_thesis: contradiction
A5: not A \/ {a} c= B by A2, A3, XBOOLE_0:def_10;
A6: not a in B
proof
assume  a in B ; ::_thesis: contradiction
then  {a} c= B by Lm1;
hence  contradiction by A1, A5, XBOOLE_1:8; ::_thesis: verum
end;
 not B c= A by A1, A4, XBOOLE_0:def_10;
hence  contradiction by A2, A6, Th135; ::_thesis: verum
end;