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 :: thesis: for Y being Subset-Family of X st x c= union Y holds
ex Z being finite Subset of Y st x c= union Z

defpred S₁[ object , object ] means ex A being set st
( A = $2 & $1 in A );
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 object st e in x holds
ex u being object st
( u in Y & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in x implies ex u being object st
( u in Y & S₁[e,u] ) )
assume e in x ; :: thesis: ex u being object 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 object 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 object st e in x holds
S₁[e,f . e] from FUNCT_1:sch 6(A5);
reconsider Z = rng f as Subset of Y by A7;
reconsider Z = Z as finite Subset of Y by A3, A6, FINSET_1:8;
take Z = Z; :: thesis: x c= union Z

now :: thesis: for z being object st z in x holds
z in union Z

let z be object ; :: thesis: ( z in x implies z in union Z )
assume A9: z in x ; :: thesis: z in union Z
then S₁[z,f . z] by A8;
then ( z in f . z & f . z in Z ) by A6, FUNCT_1:def 3, A9;
hence z in union Z by TARSKI:def 4; :: thesis: verum

end;

hence x c= union Z ; :: thesis: verum

end;

then x << x by Th27;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not t in { {y} where y is Element of x9 : verum } or t in bool X )
reconsider tt = t as set by TARSKI:1;
assume t in { {y} where y is Element of x9 : verum } ; :: thesis: t in bool X
then A10: ex y9 being Element of x9 st t = {y9} ;
for k being object st k in tt holds
k in X by A10, Th26, TARSKI:def 3;
then tt c= X ;
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 :: thesis: for y being object st y in x holds
y in union Y

let y be object ; :: 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 ;
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, Th27;

now :: thesis: for k being set st k in Z holds
k is finite

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:7;
hence x is finite by A13; :: thesis: verum

end;

end;

end;