let X be set ; :: thesis: for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
let x be Element of (BoolePoset X); :: thesis: ( x is finite iff x is compact )

per cases ( x is empty or not x is empty ) ;

suppose A1: x is empty ; :: thesis: ( x is finite iff x is compact )

then x = Bottom (BoolePoset X) by YELLOW_1:18;
hence ( x is finite iff x is compact ) by A1, WAYBEL_3:15; :: thesis: verum

end;

suppose A2: not x is empty ; :: thesis: ( x is finite iff x is compact )

thus ( x is finite implies x is compact ) :: thesis: ( x is compact implies x is finite )

proof

assume A3: x is finite ; :: thesis: x is compact

now

defpred S₁[ set , set ] means $1 in $2;
let Y be Subset-Family of X; :: thesis: ( x c= union Y implies ex Z being finite Subset of Y st x c= union Z )
assume A4: x c= union Y ; :: thesis: ex Z being finite Subset of Y st x c= union Z
A5: for e being set st e in x holds
ex u being set st
( u in Y & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in x implies ex u being set st
( u in Y & S₁[e,u] ) )
assume e in x ; :: thesis: ex u being set st
( u in Y & S₁[e,u] )
then ex u being set st
( e in u & u in Y ) by A4, TARSKI:def 4;
hence ex u being set st
( u in Y & S₁[e,u] ) ; :: thesis: verum

end;

consider f being Function such that
A6: dom f = x and
A7: rng f c= Y and
A8: for e being set st e in x holds
S₁[e,f . e] from WELLORD2:sch 1(A5);
reconsider Z = rng f as Subset of Y by A7;
reconsider Z = Z as finite Subset of Y by A3, A6, FINSET_1:26;
take Z = Z; :: thesis: x c= union Z

now

let z be set ; :: thesis: ( z in x implies z in union Z )
assume z in x ; :: thesis: z in union Z
then ( z in f . z & f . z in Z ) by A6, A8, FUNCT_1:def 5;
hence z in union Z by TARSKI:def 4; :: thesis: verum

end;

hence x c= union Z by TARSKI:def 3; :: thesis: verum

end;

then x << x by Th29;
hence x is compact by WAYBEL_3:def 2; :: thesis: verum

end;

thus ( x is compact implies x is finite ) :: thesis: verum

proof

reconsider x9 = x as non empty set by A2;
set Y = { {y} where y is Element of x9 : verum } ;
{ {y} where y is Element of x9 : verum } c= bool X

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { {y} where y is Element of x9 : verum } or t in bool X )
assume t in { {y} where y is Element of x9 : verum } ; :: thesis: t in bool X
then A9: ex y9 being Element of x9 st t = {y9} ;

now

let k be set ; :: thesis: ( k in t implies k in X )
assume A10: k in t ; :: thesis: k in X
x c= X by Th28;
hence k in X by A9, A10, TARSKI:def 3; :: thesis: verum

end;

then t c= X by TARSKI:def 3;
hence t in bool X ; :: thesis: verum

end;

then reconsider Y = { {y} where y is Element of x9 : verum } as Subset-Family of X ;

now

let y be set ; :: thesis: ( y in x implies y in union Y )
assume y in x ; :: thesis: y in union Y
then A11: {y} in Y ;
y in {y} by TARSKI:def 1;
hence y in union Y by A11, TARSKI:def 4; :: thesis: verum

end;

then A12: x c= union Y by TARSKI:def 3;
assume x is compact ; :: thesis: x is finite
then x << x by WAYBEL_3:def 2;
then consider Z being finite Subset of Y such that
A13: x c= union Z by A12, Th29;

now

let k be set ; :: thesis: ( k in Z implies k is finite )
assume k in Z ; :: thesis: k is finite
then k in Y ;
then ex y9 being Element of x9 st k = {y9} ;
hence k is finite ; :: thesis: verum

end;

then union Z is finite by FINSET_1:25;
hence x is finite by A13; :: thesis: verum

end;

end;

end;