:: ZFMISC_1 semantic presentation

begin

registration
let x, y be ( ( ) ( ) set ) ;
cluster [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) -> non empty ;
end;

definition
let X be ( ( ) ( ) set ) ;
func bool X -> ( ( ) ( ) set ) means :: ZFMISC_1:def 1
 for Z being ( ( ) ( ) set ) holds
( Z : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff Z : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) );
end;

definition
let X1, X2 be ( ( ) ( ) set ) ;
func [:X1,X2:] -> ( ( ) ( ) set ) means :: ZFMISC_1:def 2
 for z being ( ( ) ( ) set ) holds
( z : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X1 : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X2 : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) = [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) ) );
end;

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

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

begin

theorem :: ZFMISC_1:1
bool {} : ( ( ) ( empty ) set ) : ( ( ) ( ) set ) = {{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:2
union {} : ( ( ) ( empty ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: ZFMISC_1:3
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:4
for x, y1, y2 being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = {y1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = y1 : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:5
for x, y1, y2 being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = {y1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
y1 : ( ( ) ( ) set ) = y2 : ( ( ) ( ) set ) ;

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

theorem :: ZFMISC_1:7
for x, y being ( ( ) ( ) set ) holds {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:8
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \/ {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:9
for x, y being ( ( ) ( ) set ) holds {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \/ {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:10
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:11
for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:12
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) /\ {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:13
for x, y being ( ( ) ( ) set ) holds {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) /\ {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:14
for x, y being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) iff x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) ) ;

theorem :: ZFMISC_1:15
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) holds
x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:16
for x, y being ( ( ) ( ) set ) holds {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: ZFMISC_1:17
for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:18
for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:19
for z, x, y being ( ( ) ( ) set ) holds
( not {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or z : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) or z : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ) ;

theorem :: ZFMISC_1:20
for x, y, z being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = z : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:21
for x, y, z being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

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

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

theorem :: ZFMISC_1:24
for x being ( ( ) ( ) set ) holds bool {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {{} : ( ( ) ( empty ) set ) ,{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:25
for x being ( ( ) ( ) set ) holds union {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:26
for x, y being ( ( ) ( ) set ) holds union {{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ,{y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:27
canceled;

theorem :: ZFMISC_1:28
for x, y, x1, y1 being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in [:{x1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ,{y1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) set ) = x1 : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) = y1 : ( ( ) ( ) set ) ) ) ;

theorem :: ZFMISC_1:29
for x, y being ( ( ) ( ) set ) holds [:{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ,{y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) = {[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) ;

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

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

theorem :: ZFMISC_1:32
for x1, x2, Z being ( ( ) ( ) set ) holds
( {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= Z : ( ( ) ( ) set ) iff ( x1 : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) ) ) ;

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

theorem :: ZFMISC_1:34
for Y, X, x being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & not x : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) \ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ;

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

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

theorem :: ZFMISC_1:37
for z, X, Y being ( ( ) ( ) set ) holds
( not {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) or ( X : ( ( ) ( ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & Y : ( ( ) ( ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) or ( X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) & Y : ( ( ) ( ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) or ( X : ( ( ) ( ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & Y : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ) ) ;

theorem :: ZFMISC_1:38
for z, X, Y being ( ( ) ( ) set ) st {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) <> Y : ( ( ) ( ) set ) & not X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) holds
Y : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: ZFMISC_1:39
for x, X being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \/ X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) c= X : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ;

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

theorem :: ZFMISC_1:41
for x, y, Z being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) c= Z : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:42
for x, Z, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) = Z : ( ( ) ( ) set ) ;

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

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

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

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

theorem :: ZFMISC_1:47
for x, Z, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: ZFMISC_1:48
for x, X being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses X : ( ( ) ( ) set ) holds
not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:49
for x, y, Z being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses Z : ( ( ) ( ) set ) holds
not x : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:50
for x, X being ( ( ) ( ) set ) st not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses X : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:51
for x, Z, y being ( ( ) ( ) set ) st not x : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) misses Z : ( ( ) ( ) set ) ;

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

theorem :: ZFMISC_1:53
for x, y, X being ( ( ) ( ) set ) holds
( not {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) /\ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or not y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) or x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ) ;

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

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

theorem :: ZFMISC_1:56
for z, X, x being ( ( ) ( ) set ) holds
( z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) \ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) iff ( z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) <> x : ( ( ) ( ) set ) ) ) ;

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

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

theorem :: ZFMISC_1:59
for x, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) iff not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ;

theorem :: ZFMISC_1:60
for x, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) iff x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ;

theorem :: ZFMISC_1:61
for x, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) or {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ;

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

theorem :: ZFMISC_1:63
for x, y, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) iff ( not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) ;

theorem :: ZFMISC_1:64
for x, y, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) iff ( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) ;

theorem :: ZFMISC_1:65
for x, y, X being ( ( ) ( ) set ) holds
( {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) or {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ;

theorem :: ZFMISC_1:66
for X, x, y being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) \ {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) iff ( X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) or X : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or X : ( ( ) ( ) set ) = {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or X : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ;

theorem :: ZFMISC_1:67
for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) holds
bool A : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= bool B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:68
for A being ( ( ) ( ) set ) holds {A : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) c= bool A : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

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

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

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

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

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

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

theorem :: ZFMISC_1:75
for X, Y being ( ( ) ( ) set ) holds union {X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

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

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

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

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

theorem :: ZFMISC_1:80
for A, B being ( ( ) ( ) set ) st ( for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) ) holds
union A : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) ;

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

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

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

theorem :: ZFMISC_1:84
for A, X, Y, z being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) = [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) ) ;

theorem :: ZFMISC_1:85
for z, X1, Y1, X2, Y2 being ( ( ) ( ) set ) st z : ( ( ) ( ) set ) in [:X1 : ( ( ) ( ) set ) ,Y1 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) /\ [:X2 : ( ( ) ( ) set ) ,Y2 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
ex x, y being ( ( ) ( ) set ) st
( z : ( ( ) ( ) set ) = [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) & x : ( ( ) ( ) set ) in X1 : ( ( ) ( ) set ) /\ X2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y1 : ( ( ) ( ) set ) /\ Y2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

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

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

theorem :: ZFMISC_1:88
for x, y, X, Y being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) holds
[y : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:89
for X1, Y1, X2, Y2 being ( ( ) ( ) set ) st ( for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in [:X1 : ( ( ) ( ) set ) ,Y1 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) iff [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in [:X2 : ( ( ) ( ) set ) ,Y2 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ) holds
[:X1 : ( ( ) ( ) set ) ,Y1 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) = [:X2 : ( ( ) ( ) set ) ,Y2 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

begin

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

theorem :: ZFMISC_1:115
for A being ( ( non empty ) ( non empty ) set )
for B, C, D being ( ( ) ( ) set ) st ( [:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) c= [:C : ( ( ) ( ) set ) ,D : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) or [:B : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) c= [:D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) holds
B : ( ( ) ( ) set ) c= D : ( ( ) ( ) set ) ;

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

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

theorem :: ZFMISC_1:118
for x, y, z, Z being ( ( ) ( ) set ) holds
( Z : ( ( ) ( ) set ) c= {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) } : ( ( ) ( ) set ) iff ( Z : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) or Z : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {y : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) or Z : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) } : ( ( ) ( ) set ) ) ) ;

theorem :: ZFMISC_1:119
for N, M, X1, Y1, X2, Y2 being ( ( ) ( ) set ) st N : ( ( ) ( ) set ) c= [:X1 : ( ( ) ( ) set ) ,Y1 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) & M : ( ( ) ( ) set ) c= [:X2 : ( ( ) ( ) set ) ,Y2 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) holds
N : ( ( ) ( ) set ) \/ M : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= [:(X1 : ( ( ) ( ) set ) \/ X2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(Y1 : ( ( ) ( ) set ) \/ Y2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:120
for x, y, X being ( ( ) ( ) set ) st not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \ {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ;

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

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

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

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

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 : ( ( ) ( ) set ) <> x2 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x3 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x3 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x4 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x4 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x5 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) );
end;

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 : ( ( ) ( ) set ) <> x2 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x3 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x3 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) & x4 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x4 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x4 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) & x5 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x5 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) & x6 : ( ( ) ( ) set ) <> x7 : ( ( ) ( ) set ) );
end;

theorem :: ZFMISC_1:122
for x1, x2, y1, y2 being ( ( ) ( ) set ) holds [:{x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ,{y1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) = {[x1 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) ,[x1 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) ,[x2 : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) ,[x2 : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) } : ( ( ) ( ) set ) ;

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

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

registration
cluster empty -> trivial for ( ( ) ( ) set ) ;
end;

registration
cluster non trivial -> non empty for ( ( ) ( ) set ) ;
end;

registration
let x be ( ( ) ( ) set ) ;
cluster {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> trivial ;
end;

registration
cluster non empty trivial for ( ( ) ( ) set ) ;
end;

theorem :: ZFMISC_1:124
for A, B, C, p being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) /\ C : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {p : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) & p : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
A : ( ( ) ( ) set ) /\ C : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {p : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ;

theorem :: ZFMISC_1:125
for A, B, C, p being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= {p : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) & p : ( ( ) ( ) set ) in C : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) holds
A : ( ( ) ( ) set ) \/ C : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) ;

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

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( empty ) ( empty trivial ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( empty ) ( empty trivial ) set ) :] : ( ( ) ( ) set ) -> empty ;
end;

registration
let X be ( ( empty ) ( empty trivial ) set ) ;
let Y be ( ( ) ( ) set ) ;
cluster [:X : ( ( empty ) ( empty trivial ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -> empty ;
end;

theorem :: ZFMISC_1:127
for A, B being ( ( ) ( ) set ) holds not A : ( ( ) ( ) set ) in [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:128
for x being ( ( ) ( ) set ) holds [x : ( ( ) ( ) set ) ,{x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ] : ( ( ) ( non empty ) set ) in [:{x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ,[x : ( ( ) ( ) set ) ,{x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ] : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ;

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

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

registration
cluster non trivial for ( ( ) ( ) set ) ;
end;

theorem :: ZFMISC_1:131
for X being ( ( ) ( ) set ) st not X : ( ( ) ( ) set ) is empty & X : ( ( ) ( ) set ) is trivial holds
ex x being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ;

theorem :: ZFMISC_1:132
for x being ( ( ) ( ) set )
for X being ( ( trivial ) ( trivial ) set ) st x : ( ( ) ( ) set ) in X : ( ( trivial ) ( trivial ) set ) holds
X : ( ( trivial ) ( trivial ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) ;

theorem :: ZFMISC_1:133
for a, b, c, X being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & c : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
{a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) } : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ;

theorem :: ZFMISC_1:134
for x, y, X being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( non empty ) set ) in X : ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in union (union X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in union (union X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: ZFMISC_1:135
for Y, x, X being ( ( ) ( ) set ) holds
( not X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) : ( ( ) ( non empty ) set ) or x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) or X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ) ;

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

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

theorem :: ZFMISC_1:138
for A, B, a being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) \/ {a : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) : ( ( ) ( non empty ) set ) & not A : ( ( ) ( ) set ) \/ {a : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) : ( ( ) ( non empty ) set ) = B : ( ( ) ( ) set ) holds
A : ( ( ) ( ) set ) = B : ( ( ) ( ) set ) ;