let S be lower-bounded sup-Semilattice; :: thesis: for x being Element of (InclPoset (Ids S)) holds
( x is compact iff x is principal Ideal of S )
reconsider InIdS = InclPoset (Ids S) as CLSubFrame of BoolePoset the carrier of S by Th8;
let x be Element of (InclPoset (Ids S)); :: thesis: ( x is compact iff x is principal Ideal of S )
reconsider x9 = x as Ideal of S by YELLOW_2:41;
thus ( x is compact implies x is principal Ideal of S ) :: thesis: ( x is principal Ideal of S implies x is compact )

proof

assume x is compact ; :: thesis: x is principal Ideal of S
then x in the carrier of (CompactSublatt InIdS) by WAYBEL_8:def 1;
then consider F being Element of (BoolePoset the carrier of S) such that
A1: F is finite and
A2: x = meet { Y where Y is Element of InIdS : F c= Y } and
A3: F c= x by Th7;
A4: F c= the carrier of S by WAYBEL_8:26;
ex y being Element of S st
( y in x9 & y is_>=_than x9 )

proof

reconsider F9 = F as Subset of S by WAYBEL_8:26;
reconsider F9 = F9 as Subset of S ;
reconsider y = sup F9 as Element of S ;
take y ; :: thesis: ( y in x9 & y is_>=_than x9 )

now :: thesis: y in x9

per cases ( F9 <> {} or F9 = {} ) ;

suppose F9 <> {} ; :: thesis: y in x9

hence y in x9 by A1, A3, WAYBEL_0:42; :: thesis: verum

end;

suppose F9 = {} ; :: thesis: y in x9

then y = Bottom S by YELLOW_0:def 11;
hence y in x9 by WAYBEL_4:21; :: thesis: verum

end;

end;

end;

hence y in x9 ; :: thesis: y is_>=_than x9

now :: thesis: for b being Element of S st b in x9 holds
b <= y

now :: thesis: for u being object st u in F holds
u in downarrow y

let u be object ; :: thesis: ( u in F implies u in downarrow y )
assume A5: u in F ; :: thesis: u in downarrow y
then reconsider u9 = u as Element of S by A4;
ex_sup_of F9,S by A1, A5, YELLOW_0:54;
then y is_>=_than F by YELLOW_0:30;
then u9 <= y by A5, LATTICE3:def 9;
hence u in downarrow y by WAYBEL_0:17; :: thesis: verum

end;

then A6: F c= downarrow y ;
let b be Element of S; :: thesis: ( b in x9 implies b <= y )
assume A7: b in x9 ; :: thesis: b <= y
downarrow y is Element of InIdS by YELLOW_2:41;
then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A6;
then b in downarrow y by A2, A7, SETFAM_1:def 1;
hence b <= y by WAYBEL_0:17; :: thesis: verum

end;

hence y is_>=_than x9 by LATTICE3:def 9; :: thesis: verum

end;

hence x is principal Ideal of S by WAYBEL_0:def 21; :: thesis: verum

end;

thus ( x is principal Ideal of S implies x is compact ) :: thesis: verum

proof

assume x is principal Ideal of S ; :: thesis: x is compact
then consider y being Element of S such that
A8: y in x9 and
A9: y is_>=_than x9 by WAYBEL_0:def 21;
ex F being Element of (BoolePoset the carrier of S) st
( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )

proof

reconsider F = {y} as Element of (BoolePoset the carrier of S) by WAYBEL_8:26;
take F ; :: thesis: ( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )
thus F is finite ; :: thesis: ( F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )
for v being object st v in F holds
v in x by A8, TARSKI:def 1;
hence A10: F c= x ; :: thesis: x = meet { Y where Y is Element of InIdS : F c= Y }

A11: now :: thesis: for z being object holds
( ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) & ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x ) )

let z be object ; :: thesis: ( ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) & ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x ) )
thus ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) :: thesis: ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x )

proof

assume A12: z in x ; :: thesis: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z
then reconsider z9 = z as Element of S by YELLOW_2:42;
A13: z9 <= y by A9, A12, LATTICE3:def 9;
let Z be set ; :: thesis: ( Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z )
assume Z in { Y where Y is Element of InIdS : F c= Y } ; :: thesis: z in Z
then consider Z1 being Element of InIdS such that
A14: ( Z1 = Z & F c= Z1 ) ;
( Z1 is Ideal of S & y in F ) by TARSKI:def 1, YELLOW_2:41;
hence z in Z by A14, A13, WAYBEL_0:def 19; :: thesis: verum

end;

thus ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x ) :: thesis: verum

proof

assume A15: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ; :: thesis: z in x
x in { Y where Y is Element of InIdS : F c= Y } by A10;
hence z in x by A15; :: thesis: verum

end;

end;

[#] S is Element of InIdS by YELLOW_2:41;
then [#] S in { Y where Y is Element of InIdS : F c= Y } ;
hence x = meet { Y where Y is Element of InIdS : F c= Y } by A11, SETFAM_1:def 1; :: thesis: verum

end;

then x in the carrier of (CompactSublatt InIdS) by Th7;
hence x is compact by WAYBEL_8:def 1; :: thesis: verum

end;