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 )
reconsider F9 = F as Element of (BoolePoset X) by Th26;
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 F9 = F as Element of (BoolePoset X) by A2;
( F9 <= F9 & F9 is compact ) by A2, Def1;
then F9 in compactbelow F9 ;
then F9 in { y where y is finite Subset of F9 : verum } by Th29;
then ex F1 being finite Subset of F9 st F1 = F9 ;
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 F9 : verum } by A1;
then F9 in compactbelow F9 by Th29;
then F9 is compact by Th4;
hence F in the carrier of (CompactSublatt (BoolePoset X)) by Def1; :: thesis: verum