let X be set ; :: thesis: for F being Subset of holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
let F be Subset of ; :: thesis: ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
reconsider F' = F as Element of by Th28;
A1: F c= F ;
thus ( F in the carrier of (CompactSublatt (BoolePoset X)) implies F is finite ) :: thesis: ( F is finite implies F in the carrier of (CompactSublatt (BoolePoset X)) )

proof

assume A2: F in the carrier of (CompactSublatt (BoolePoset X)) ; :: thesis: F is finite
the carrier of (CompactSublatt (BoolePoset X)) c= the carrier of (BoolePoset X) by YELLOW_0:def 13;
then reconsider F' = F as Element of by A2;
( F' <= F' & F' is compact ) by A2, Def1;
then F' in compactbelow F' ;
then F' in { y where y is finite Subset of : verum } by Th31;
then ex F1 being finite Subset of st F1 = F' ;
hence F is finite ; :: thesis: verum

end;

assume F is finite ; :: thesis: F in the carrier of (CompactSublatt (BoolePoset X))
then F in { y where y is finite Subset of : verum } by A1;
then F' in compactbelow F' by Th31;
then F' is compact by Th4;
hence F in the carrier of (CompactSublatt (BoolePoset X)) by Def1; :: thesis: verum