let X be set ; :: thesis: for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
let F be Subset of X; :: thesis: ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
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 A1: 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 (BoolePoset X) by A1;
( F' <= F' & F' is compact ) by A1, Def1;
then F' in compactbelow F' ;
then F' in { y where y is finite Subset of F' : verum } by Th31;
then consider F1 being finite Subset of F' such that
A2: F1 = F' ;
thus F is finite by A2; :: thesis: verum

end;

assume A3: F is finite ; :: thesis: F in the carrier of (CompactSublatt (BoolePoset X))
reconsider F' = F as Element of (BoolePoset X) by Th28;
F c= F ;
then F in { y where y is finite Subset of F' : verum } by A3;
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