:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Copyright (c) 1990 Association of Mizar Users

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 end;

Lm2: for Y, X, x being set st Y c= X & not x in Y holds
Y c= X \ {x}
proof end;

Lm3: for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )
proof 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 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 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 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 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
proof end;

theorem :: ZFMISC_1:2
proof end;

theorem :: ZFMISC_1:3
canceled;

theorem :: ZFMISC_1:4
canceled;

theorem :: ZFMISC_1:5
canceled;

theorem Th6: :: ZFMISC_1:6
for x, y being set st {x} c= {y} holds
x = y
proof end;

theorem :: ZFMISC_1:7
canceled;

theorem Th8: :: ZFMISC_1:8
for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1
proof end;

theorem Th9: :: ZFMISC_1:9
for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2
proof end;

theorem Th10: :: ZFMISC_1:10
for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
proof end;

theorem :: ZFMISC_1:11
canceled;

theorem Th12: :: ZFMISC_1:12
for x, y being set holds {x} c= {x,y}
proof end;

Lm4: for x, X being set st {x} \/ X c= X holds
x in X
proof end;

theorem :: ZFMISC_1:13
for x, y being set st {x} \/ {y} = {x} holds
x = y
proof end;

Lm5: for x, X being set st x in X holds
{x} \/ X = X
proof end;

theorem :: ZFMISC_1:14
for x, y being set holds {x} \/ {x,y} = {x,y}
proof end;

Lm6: for x, X being set st {x} misses X holds
not x in X
proof end;

theorem :: ZFMISC_1:15
canceled;

theorem :: ZFMISC_1:16
for x, y being set st {x} misses {y} holds
x <> y
proof end;

Lm7: for x, X being set st not x in X holds
{x} misses X
proof end;

theorem Th17: :: ZFMISC_1:17
for x, y being set st x <> y holds
{x} misses {y}
proof end;

Lm8: for X, x being set st X /\ {x} = {x} holds
x in X
proof end;

theorem :: ZFMISC_1:18
for x, y being set st {x} /\ {y} = {x} holds
x = y
proof end;

Lm9: for x, X being set st x in X holds
X /\ {x} = {x}
proof end;

theorem :: ZFMISC_1:19
for x, y being set holds {x} /\ {x,y} = {x}
proof end;

Lm10: for x, X being set holds
( {x} \ X = {x} iff not x in X )
proof end;

theorem :: ZFMISC_1:20
for x, y being set holds
( {x} \ {y} = {x} iff x <> y )
proof end;

Lm11: for x, X being set holds
( {x} \ X = {} iff x in X )
proof end;

theorem :: ZFMISC_1:21
for x, y being set st {x} \ {y} = {} holds
x = y
proof end;

theorem :: ZFMISC_1:22
for x, y being set holds {x} \ {x,y} = {}
proof 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 end;

theorem :: ZFMISC_1:23
for x, y being set st x <> y holds
{x,y} \ {y} = {x}
proof end;

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

theorem :: ZFMISC_1:25
for z, x, y being set holds
( not {z} c= {x,y} or z = x or z = y )
proof end;

theorem Th26: :: ZFMISC_1:26
for x, y, z being set st {x,y} c= {z} holds
x = z
proof end;

theorem :: ZFMISC_1:27
for x, y, z being set st {x,y} c= {z} holds
{x,y} = {z}
proof end;

Lm13: for X, x being set st X <> {x} & X <> {} holds
ex y being set st
( y in X & y <> x )
proof 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 end;

theorem :: ZFMISC_1:28
for x1, x2, y1, y2 being set holds
( not {x1,x2} c= {y1,y2} or x1 = y1 or x1 = y2 )
proof end;

theorem :: ZFMISC_1:29
for x, y being set st x <> y holds
{x} \+\ {y} = {x,y}
proof end;

theorem :: ZFMISC_1:30
for x being set holds bool {x} = {{},{x}}
proof end;

Lm15: for X, A being set st X in A holds
X c= union A
proof end;

theorem :: ZFMISC_1:31
for x being set holds union {x} = x
proof end;

Lm16: for X, Y being set holds union {X,Y} = X \/ Y
proof end;

theorem :: ZFMISC_1:32
for x, y being set holds union {{x},{y}} = {x,y}
proof end;

theorem Th33: :: ZFMISC_1:33
for x1, x2, y1, y2 being set st [x1,x2] = [y1,y2] holds
( x1 = y1 & x2 = y2 )
proof end;

Lm17: for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
proof end;

theorem :: ZFMISC_1:34
for x, y, x1, y1 being set holds
( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )
proof end;

theorem :: ZFMISC_1:35
for x, y being set holds [:{x},{y}:] = {[x,y]}
proof end;

theorem Th36: :: ZFMISC_1:36
for x, y, z being set holds
( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )
proof end;

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

theorem Th38: :: ZFMISC_1:38
for x1, x2, Z being set holds
( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )
proof end;

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

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

theorem :: ZFMISC_1:41
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:42
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 Th43: :: ZFMISC_1:43
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 end;

theorem :: ZFMISC_1:44
for z, X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}
proof end;

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

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

theorem :: ZFMISC_1:47
for x, y, Z being set st {x,y} \/ Z c= Z holds
x in Z
proof end;

theorem :: ZFMISC_1:48
for x, Z, y being set st x in Z & y in Z holds
{x,y} \/ Z = Z
proof end;

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

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

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

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

theorem :: ZFMISC_1:53
for x, Z, y being set st x in Z & y in Z holds
{x,y} /\ Z = {x,y}
proof end;

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

theorem Th55: :: ZFMISC_1:55
for x, y, Z being set st {x,y} misses Z holds
not x in Z
proof end;

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

theorem Th57: :: ZFMISC_1:57
for x, Z, y being set st not x in Z & not y in Z holds
{x,y} misses Z
proof end;

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

theorem :: ZFMISC_1:59
for x, y, X being set holds
( not {x,y} /\ X = {x} or not y in X or x = y )
proof end;

theorem :: ZFMISC_1:60
for x, X, y being set st x in X & ( not y in X or x = y ) holds
{x,y} /\ X = {x}
proof end;

theorem :: ZFMISC_1:61
canceled;

theorem :: ZFMISC_1:62
canceled;

theorem :: ZFMISC_1:63
for x, y, X being set st {x,y} /\ X = {x,y} holds
x in X
proof end;

theorem Th64: :: ZFMISC_1:64
for z, X, x being set holds
( z in X \ {x} iff ( z in X & z <> x ) )
proof end;

theorem Th65: :: ZFMISC_1:65
for X, x being set holds
( X \ {x} = X iff not x in X )
proof end;

theorem :: ZFMISC_1:66
for X, x being set holds
( not X \ {x} = {} or X = {} or X = {x} )
proof end;

theorem :: ZFMISC_1:67
for x, X being set holds
( {x} \ X = {x} iff not x in X ) by Lm10;

theorem :: ZFMISC_1:68
for x, X being set holds
( {x} \ X = {} iff x in X ) by Lm11;

theorem :: ZFMISC_1:69
for x, X being set holds
( {x} \ X = {} or {x} \ X = {x} )
proof end;

theorem :: ZFMISC_1:70
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:71
canceled;

theorem Th72: :: ZFMISC_1:72
for x, y, X being set holds
( {x,y} \ X = {x,y} iff ( not x in X & not y in X ) )
proof end;

theorem Th73: :: ZFMISC_1:73
for x, y, X being set holds
( {x,y} \ X = {} iff ( x in X & y in X ) )
proof end;

theorem :: ZFMISC_1:74
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 end;

theorem :: ZFMISC_1:75
for X, x, y being set holds
( X \ {x,y} = {} iff ( X = {} or X = {x} or X = {y} or X = {x,y} ) )
proof end;

theorem :: ZFMISC_1:76
canceled;

theorem :: ZFMISC_1:77
canceled;

theorem :: ZFMISC_1:78
canceled;

theorem :: ZFMISC_1:79
for A, B being set st A c= B holds
bool A c= bool B
proof end;

theorem :: ZFMISC_1:80
for A being set holds {A} c= bool A
proof end;

theorem :: ZFMISC_1:81
for A, B being set holds (bool A) \/ (bool B) c= bool (A \/ B)
proof end;

theorem :: ZFMISC_1:82
for A, B being set st (bool A) \/ (bool B) = bool (A \/ B) holds
A,B are_c=-comparable
proof end;

theorem :: ZFMISC_1:83
for A, B being set holds bool (A /\ B) = (bool A) /\ (bool B)
proof end;

theorem :: ZFMISC_1:84
for A, B being set holds bool (A \ B) c= \/ ((bool A) \ (bool B))
proof end;

theorem :: ZFMISC_1:85
canceled;

theorem :: ZFMISC_1:86
for A, B being set holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proof end;

theorem :: ZFMISC_1:87
canceled;

theorem :: ZFMISC_1:88
canceled;

theorem :: ZFMISC_1:89
canceled;

theorem :: ZFMISC_1:90
canceled;

theorem :: ZFMISC_1:91
canceled;

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

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

theorem :: ZFMISC_1:94
for A, Z being set st ( for X being set st X in A holds
X c= Z ) holds
union A c= Z
proof end;

theorem Th95: :: ZFMISC_1:95
for A, B being set st A c= B holds
union A c= union B
proof end;

theorem :: ZFMISC_1:96
for A, B being set holds union (A \/ B) = () \/ ()
proof end;

theorem Th97: :: ZFMISC_1:97
for A, B being set holds union (A /\ B) c= () /\ ()
proof end;

theorem Th98: :: ZFMISC_1:98
for A, B being set st ( for X being set st X in A holds
X misses B ) holds
union A misses B
proof end;

theorem :: ZFMISC_1:99
for A being set holds union (bool A) = A
proof end;

theorem :: ZFMISC_1:100
for A being set holds A c= bool ()
proof end;

theorem :: ZFMISC_1:101
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) = () /\ ()
proof end;

theorem :: ZFMISC_1:102
canceled;

theorem Th103: :: ZFMISC_1:103
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 end;

theorem Th104: :: ZFMISC_1:104
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 end;

theorem :: ZFMISC_1:105
for X, Y being set holds [:X,Y:] c= bool (bool (X \/ Y))
proof end;

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

theorem Th107: :: ZFMISC_1:107
for x, y, X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]
proof end;

theorem :: ZFMISC_1:108
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 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 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 end;

theorem :: ZFMISC_1:109
canceled;

theorem :: ZFMISC_1:110
canceled;

theorem :: ZFMISC_1:111
canceled;

theorem :: ZFMISC_1:112
canceled;

theorem Th113: :: ZFMISC_1:113
for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )
proof end;

theorem :: ZFMISC_1:114
for X, Y being set st X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] holds
X = Y
proof end;

theorem :: ZFMISC_1:115
for X, Y being set st [:X,X:] = [:Y,Y:] holds
X = Y
proof end;

Lm20: for z, X, Y being set st z in [:X,Y:] holds
ex x, y being set st [x,y] = z
proof end;

theorem :: ZFMISC_1:116
for X being set st X c= [:X,X:] holds
X = {}
proof end;

theorem :: ZFMISC_1:117
for Z, X, Y being set st Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) holds
X c= Y
proof end;

theorem Th118: :: ZFMISC_1:118
for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )
proof end;

theorem Th119: :: ZFMISC_1:119
for X1, Y1, X2, Y2 being set st X1 c= Y1 & X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]
proof end;

theorem Th120: :: ZFMISC_1:120
for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
proof end;

theorem :: ZFMISC_1:121
for X1, X2, Y1, Y2 being set holds [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]
proof end;

theorem :: ZFMISC_1:122
for X, Y, Z being set holds
( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
proof end;

theorem Th123: :: ZFMISC_1:123
for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]
proof end;

theorem :: ZFMISC_1:124
for A, X, B, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]
proof end;

theorem Th125: :: ZFMISC_1:125
for X, Y, Z being set holds
( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )
proof end;

theorem :: ZFMISC_1:126
for X1, X2, Y1, Y2 being set holds [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
proof end;

theorem Th127: :: ZFMISC_1:127
for X1, X2, Y1, Y2 being set st ( X1 misses X2 or Y1 misses Y2 ) holds
[:X1,Y1:] misses [:X2,Y2:]
proof end;

theorem Th128: :: ZFMISC_1:128
for x, y, z, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
proof end;

theorem Th129: :: ZFMISC_1:129
for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
proof end;

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

theorem :: ZFMISC_1:131
for x, y, X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
proof end;

theorem :: ZFMISC_1:132
for x, y, X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
proof end;

theorem :: ZFMISC_1:133
canceled;

theorem Th134: :: ZFMISC_1:134
for X1, Y1, X2, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 & Y1 = Y2 )
proof end;

theorem :: ZFMISC_1:135
for X, Y being set st ( X c= [:X,Y:] or X c= [:Y,X:] ) holds
X = {}
proof end;

theorem :: ZFMISC_1:136
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 end;

theorem :: ZFMISC_1:137
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 end;

begin

theorem Th138: :: ZFMISC_1:138
for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} holds
( X1 c= Y1 & X2 c= Y2 )
proof end;

theorem :: ZFMISC_1:139
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 end;

theorem :: ZFMISC_1:140
for x, X being set st x in X holds
(X \ {x}) \/ {x} = X
proof end;

theorem :: ZFMISC_1:141
for x, X being set st not x in X holds
(X \/ {x}) \ {x} = X
proof end;

theorem :: ZFMISC_1:142
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 end;

theorem :: ZFMISC_1:143
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 end;

Lm21: for x, y, X being set st not x in X & not y in X holds
{x,y} misses X
proof end;

theorem Th144: :: ZFMISC_1:144
for x, y, X being set st not x in X & not y in X holds
X = X \ {x,y}
proof end;

theorem :: ZFMISC_1:145
for x, y, X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}
proof end;

definition
let x1, x2, x3 be set ;
pred x1,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 ;
pred x1,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 ;
pred x1,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 ;
pred x1,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 ;
pred x1,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:146
for x1, x2, y1, y2 being set holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof end;

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

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

:: deftheorem 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 set ;
coherence
for b1 being set st b1 is empty holds
b1 is trivial
proof end;
end;

registration
let x be set ;
cluster {x} -> trivial ;
coherence
{x} is trivial
proof end;
end;

theorem :: ZFMISC_1:148
for A, B, C, p being set st A c= B & B /\ C = {p} & p in A holds
A /\ C = {p}
proof end;

theorem :: ZFMISC_1:149
for A, B, C, p being set st A /\ B c= {p} & p in C & C misses B holds
A \/ C misses B
proof end;

theorem :: ZFMISC_1:150
canceled;

theorem :: ZFMISC_1:151
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 end;

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

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

theorem :: ZFMISC_1:152
for A, B being set holds not A in [:A,B:]
proof end;

theorem :: ZFMISC_1:153
for x being set holds [x,{x}] in [:{x},[x,{x}]:]
proof end;

theorem :: ZFMISC_1:154
for B, A being set st B in [:A,B:] holds
ex x being set st
( x in A & B = [x,{x}] )
proof end;