:: Some Basic Properties of Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990-2012 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 )
proofend;

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

Lm3:  for Y, x being set holds
( Y c= {x} iff ( Y = {} or Y = {x} ) )
proofend;

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 )
proofend;
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
proofend;
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] ) )
proofend;
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
proofend;
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

::
:: Empty set.
::
theorem :: ZFMISC_1:1
bool {} = {{}}
proofend;

theorem :: ZFMISC_1:2
union {} = {}
proofend;

::
:: Singleton and unordered pairs.
::
theorem Th3: :: ZFMISC_1:3
for x, y being set st {x} c= {y} holds
x = y
proofend;

theorem Th4: :: ZFMISC_1:4
for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1
proofend;

theorem :: ZFMISC_1:5
for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2
proofend;

theorem Th6: :: ZFMISC_1:6
for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
proofend;

theorem Th7: :: ZFMISC_1:7
for x, y being set holds {x} c= {x,y}
proofend;

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

theorem :: ZFMISC_1:8
for x, y being set st {x} \/ {y} = {x} holds
x = y
proofend;

theorem :: ZFMISC_1:9
for x, y being set holds {x} \/ {x,y} = {x,y}
proofend;

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

theorem :: ZFMISC_1:10
for x, y being set st {x} misses {y} holds
x <> y
proofend;

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

theorem Th11: :: ZFMISC_1:11
for x, y being set st x <> y holds
{x} misses {y}
proofend;

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

theorem :: ZFMISC_1:12
for x, y being set st {x} /\ {y} = {x} holds
x = y
proofend;

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}
proofend;

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 )
proofend;

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

theorem :: ZFMISC_1:16
for x, y being set holds {x} \ {x,y} = {}
proofend;

Lm12:  for x, y, X being set holds
( {x,y} \ X = {x} iff ( not x in X &amp; ( y in X or x = y ) ) )
proofend;

theorem :: ZFMISC_1:17
for x, y being set st x <> y holds
{x,y} \ {y} = {x}
proofend;

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 )
proofend;

theorem Th20: :: ZFMISC_1:20
for x, y, z being set st {x,y} c= {z} holds
x = z
proofend;

theorem :: ZFMISC_1:21
for x, y, z being set st {x,y} c= {z} holds
{x,y} = {z}
proofend;

Lm13:  for X, x being set st X <> {x} &amp; X <> {} holds
ex y being set st
( y in X &amp; y <> x )
proofend;

Lm14:  for Z, x1, x2 being set holds
( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
proofend;

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

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

theorem :: ZFMISC_1:24
for x being set holds bool {x} = {{},{x}}
proofend;

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

theorem :: ZFMISC_1:25
for x being set holds union {x} = x
proofend;

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

theorem :: ZFMISC_1:26
for x, y being set holds union {{x},{y}} = {x,y}
proofend;

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

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 &amp; y = y1 ) )
proofend;

theorem :: ZFMISC_1:29
for x, y being set holds [:{x},{y}:] = {[x,y]}
proofend;

theorem Th30: :: ZFMISC_1:30
for x, y, z being set holds
( [:{x},{y,z}:] = {[x,y],[x,z]} &amp; [:{x,y},{z}:] = {[x,z],[y,z]} )
proofend;

::
:: Singleton and unordered pairs included in a set.
::
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 &amp; x2 in Z ) )
proofend;

::
:: Set included in a singleton (or unordered pair).
::
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 &amp; not x in Y holds
Y c= X \ {x} by Lm2;

theorem :: ZFMISC_1:35
for X, x being set st X <> {x} &amp; X <> {} holds
ex y being set st
( y in X &amp; 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;

::
:: Sum of an unordered pair (or a singleton) and a set.
::
theorem Th37: :: ZFMISC_1:37
for z, X, Y being set holds
( not {z} = X \/ Y or ( X = {z} &amp; Y = {z} ) or ( X = {} &amp; Y = {z} ) or ( X = {z} &amp; Y = {} ) )
proofend;

theorem :: ZFMISC_1:38
for z, X, Y being set st {z} = X \/ Y &amp; X <> Y &amp; not X = {} holds
Y = {}
proofend;

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

theorem :: ZFMISC_1:42
for x, Z, y being set st x in Z &amp; 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 <> {} ;

::
:: Intersection of an unordered pair (or a singleton) and a set.
::
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 &amp; 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
proofend;

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 &amp; not y in Z holds
{x,y} misses Z
proofend;

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 )
proofend;

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

theorem :: ZFMISC_1:55
for x, y, X being set st {x,y} /\ X = {x,y} holds
x in X
proofend;

::
:: Difference of an unordered pair (or a singleton) and a set.
::
theorem Th56: :: ZFMISC_1:56
for z, X, x being set holds
( z in X \ {x} iff ( z in X &amp; z <> x ) )
proofend;

theorem Th57: :: ZFMISC_1:57
for X, x being set holds
( X \ {x} = X iff not x in X )
proofend;

theorem :: ZFMISC_1:58
for X, x being set holds
( not X \ {x} = {} or X = {} or X = {x} )
proofend;

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 &amp; ( 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 &amp; 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 &amp; y in X ) )
proofend;

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} )
proofend;

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} ) )
proofend;

::
:: Power Set.
::
theorem :: ZFMISC_1:67
for A, B being set st A c= B holds
bool A c= bool B
proofend;

theorem :: ZFMISC_1:68
for A being set holds {A} c= bool A
proofend;

theorem :: ZFMISC_1:69
for A, B being set holds (bool A) \/ (bool B) c= bool (A \/ B)
proofend;

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

theorem :: ZFMISC_1:71
for A, B being set holds bool (A /\ B) = (bool A) /\ (bool B)
proofend;

theorem :: ZFMISC_1:72
for A, B being set holds bool (A \ B) c= {{}} \/ ((bool A) \ (bool B))
proofend;

theorem :: ZFMISC_1:73
for A, B being set holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proofend;

::
:: Union of a set.
::
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
proofend;

theorem Th77: :: ZFMISC_1:77
for A, B being set st A c= B holds
union A c= union B
proofend;

theorem :: ZFMISC_1:78
for A, B being set holds union (A \/ B) = (union A) \/ (union B)
proofend;

theorem Th79: :: ZFMISC_1:79
for A, B being set holds union (A /\ B) c= (union A) /\ (union B)
proofend;

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

theorem :: ZFMISC_1:81
for A being set holds union (bool A) = A
proofend;

theorem :: ZFMISC_1:82
for A being set holds A c= bool (union A)
proofend;

theorem :: ZFMISC_1:83
for A, B being set st ( for X, Y being set st X <> Y &amp; X in A \/ B &amp; Y in A \/ B holds
X misses Y ) holds
union (A /\ B) = (union A) /\ (union B)
proofend;

::
:: Cartesian product.
::
theorem Th84: :: ZFMISC_1:84
for A, X, Y, z being set st A c= [:X,Y:] &amp; z in A holds
ex x, y being set st
( x in X &amp; y in Y &amp; z = [x,y] )
proofend;

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] &amp; x in X1 /\ X2 &amp; y in Y1 /\ Y2 )
proofend;

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

theorem :: ZFMISC_1:87
for x, y, X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X &amp; 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:]
proofend;

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:]
proofend;

Lm18:  for A, X1, Y1, B, X2, Y2 being set st A c= [:X1,Y1:] &amp; B c= [:X2,Y2:] &amp; ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
proofend;

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] ) &amp; ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) &amp; ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B
proofend;

theorem Th90: :: ZFMISC_1:90
for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )
proofend;

theorem :: ZFMISC_1:91
for X, Y being set st X <> {} &amp; Y <> {} &amp; [:X,Y:] = [:Y,X:] holds
X = Y
proofend;

theorem :: ZFMISC_1:92
for X, Y being set st [:X,X:] = [:Y,Y:] holds
X = Y
proofend;

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

theorem :: ZFMISC_1:93
for X being set st X c= [:X,X:] holds
X = {}
proofend;

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

theorem Th95: :: ZFMISC_1:95
for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] &amp; [:Z,X:] c= [:Z,Y:] )
proofend;

theorem Th96: :: ZFMISC_1:96
for X1, Y1, X2, Y2 being set st X1 c= Y1 &amp; X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]
proofend;

theorem Th97: :: ZFMISC_1:97
for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] &amp; [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )
proofend;

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

theorem :: ZFMISC_1:99
for X, Y, Z being set holds
( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] &amp; [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
proofend;

theorem Th100: :: ZFMISC_1:100
for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]
proofend;

theorem :: ZFMISC_1:101
for A, X, B, Y being set st A c= X &amp; B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]
proofend;

theorem Th102: :: ZFMISC_1:102
for X, Y, Z being set holds
( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] &amp; [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )
proofend;

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

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:]
proofend;

theorem :: ZFMISC_1:105
for x, y, z, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z &amp; y in Y ) )
proofend;

theorem :: ZFMISC_1:106
for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X &amp; y = z ) )
proofend;

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

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

theorem :: ZFMISC_1:109
for x, y, X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] &amp; [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
proofend;

theorem Th110: :: ZFMISC_1:110
for X1, Y1, X2, Y2 being set st X1 <> {} &amp; Y1 <> {} &amp; [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 &amp; Y1 = Y2 )
proofend;

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

theorem :: ZFMISC_1:112
for N being set ex M being set st
( N in M &amp; ( for X, Y being set st X in M &amp; Y c= X holds
Y in M ) &amp; ( for X being set st X in M holds
bool X in M ) &amp; ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
proofend;

theorem :: ZFMISC_1:113
for e, X1, Y1, X2, Y2 being set st e in [:X1,Y1:] &amp; e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]
proofend;

begin

:: from BORSUK_1
theorem Th114: :: ZFMISC_1:114
for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] &amp; [:X1,X2:] <> {} holds
( X1 c= Y1 &amp; X2 c= Y2 )
proofend;

:: from ALTCAT_1
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
proofend;

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

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

:: from WAYBEL18, 2006.01.06, A.T.
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} ) )
proofend;

:: from PARTFUN1, 2006.12.05, A.T.
theorem :: ZFMISC_1:119
for N, M, X1, Y1, X2, Y2 being set st N c= [:X1,Y1:] &amp; M c= [:X2,Y2:] holds
N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]
proofend;

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

theorem Th120: :: ZFMISC_1:120
for x, y, X being set st not x in X &amp; not y in X holds
X = X \ {x,y}
proofend;

theorem :: ZFMISC_1:121
for x, y, X being set st not x in X &amp; not y in X holds
X = (X \/ {x,y}) \ {x,y}
proofend;

:: from INCPROJ, 2007.01.18. AK
definition
let x1, x2, x3 be set ;
predx1,x2,x3 are_mutually_different  means :: ZFMISC_1:def 5
( x1 <> x2 &amp; x1 <> x3 &amp; 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 &amp; x1 <> x3 &amp; x2 <> x3 ) );

definition
let x1, x2, x3, x4 be set ;
predx1,x2,x3,x4 are_mutually_different  means :: ZFMISC_1:def 6
( x1 <> x2 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x2 <> x3 &amp; x2 <> x4 &amp; 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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x3 <> x4 ) );

:: from CARD_2, 2007.01.18. AK
definition
let x1, x2, x3, x4, x5 be set ;
predx1,x2,x3,x4,x5 are_mutually_different  means :: ZFMISC_1:def 7
( x1 <> x2 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x3 <> x4 &amp; x3 <> x5 &amp; 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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x4 <> x5 ) );

:: from BORSUK_5, 2007.01.18. AK
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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x1 <> x6 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x2 <> x6 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x3 <> x6 &amp; x4 <> x5 &amp; x4 <> x6 &amp; 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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x1 <> x6 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x2 <> x6 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x3 <> x6 &amp; x4 <> x5 &amp; x4 <> x6 &amp; 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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x1 <> x6 &amp; x1 <> x7 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x2 <> x6 &amp; x2 <> x7 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x3 <> x6 &amp; x3 <> x7 &amp; x4 <> x5 &amp; x4 <> x6 &amp; x4 <> x7 &amp; x5 <> x6 &amp; x5 <> x7 &amp; 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 &amp; x1 <> x3 &amp; x1 <> x4 &amp; x1 <> x5 &amp; x1 <> x6 &amp; x1 <> x7 &amp; x2 <> x3 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x2 <> x6 &amp; x2 <> x7 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x3 <> x6 &amp; x3 <> x7 &amp; x4 <> x5 &amp; x4 <> x6 &amp; x4 <> x7 &amp; x5 <> x6 &amp; x5 <> x7 &amp; x6 <> x7 ) );

:: missing, 2007.02.11, A.T.
theorem :: ZFMISC_1:122
for x1, x2, y1, y2 being set holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proofend;

:: missing, 2008.03.22, A.T.
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;

:: comp. REALSET1, 2008.07.05, A.T.
definition
let X be set ;
attrX is trivial  means :Def10: :: ZFMISC_1:def 10
 for x, y being set st x in X &amp; 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 &amp; 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
proofend;
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
proofend;
end;

registration
cluster non empty trivial for set ;
existence
 ex b1 being set st
( b1 is trivial &amp; not b1 is empty )
proofend;
end;

:: from SPRECT_3, 2008.09.30, A.T.
theorem :: ZFMISC_1:124
for A, B, C, p being set st A c= B &amp; B /\ C = {p} &amp; p in A holds
A /\ C = {p}
proofend;

:: from SPRECT_2, 2008.09.30, A.T.
theorem :: ZFMISC_1:125
for A, B, C, p being set st A /\ B c= {p} &amp; p in C &amp; C misses B holds
A \/ C misses B
proofend;

theorem :: ZFMISC_1:126
for A, B being set st ( for x, y being set st x in A &amp; y in B holds
x misses y ) holds
union A misses union B
proofend;

:: from BORSUK_3, 2009.01.24, A.T.
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;

:: new, 2009.08.26, A.T
theorem :: ZFMISC_1:127
for A, B being set holds not A in [:A,B:]
proofend;

theorem :: ZFMISC_1:128
for x being set holds [x,{x}] in [:{x},[x,{x}]:]
proofend;

theorem :: ZFMISC_1:129
for B, A being set st B in [:A,B:] holds
ex x being set st
( x in A &amp; B = [x,{x}] )
proofend;

theorem :: ZFMISC_1:130
for B, A being set st B c= A &amp; A is trivial holds
B is trivial
proofend;

registration
cluster non trivial for set ;
existence
 not for b1 being set holds b1 is trivial
proofend;
end;

theorem Th131: :: ZFMISC_1:131
for X being set st not X is empty &amp; X is trivial holds
ex x being set st X = {x}
proofend;

theorem :: ZFMISC_1:132
for x being set
for X being trivial set st x in X holds
X = {x}
proofend;

:: from JORDAN16, 2011.04.27, A.T.
theorem :: ZFMISC_1:133
for a, b, c, X being set st a in X &amp; b in X &amp; c in X holds
{a,b,c} c= X
proofend;

:: Lemma from RELAT_1, FUNCT_4
theorem :: ZFMISC_1:134
for x, y, X being set st [x,y] in X holds
( x in union (union X) &amp; y in union (union X) )
proofend;

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 )
proofend;

theorem :: ZFMISC_1:136
for x, y, X being set holds
( x in X \/ {y} iff ( x in X or x = y ) )
proofend;

theorem :: ZFMISC_1:137
for x, Y, X being set holds
( X \/ {x} c= Y iff ( x in Y &amp; X c= Y ) )
proofend;

theorem :: ZFMISC_1:138
for A, B, a being set st A c= B &amp; B c= A \/ {a} &amp; not A \/ {a} = B holds
A = B
proofend;