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 )
let x be Element of (InclPoset (Ids S)); :: thesis: ( x is compact iff x is principal Ideal of S )
reconsider x' = x as Ideal of S by YELLOW_2:43;
reconsider InIdS = InclPoset (Ids S) as CLSubFrame of BoolePoset the carrier of S by Th8;
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:28;
ex y being Element of S st
( y in x' & y is_>=_than x' )

proof

reconsider F' = F as Subset of S by WAYBEL_8:28;
reconsider F' = F' as Subset of S ;
reconsider y = sup F' as Element of S ;
take y ; :: thesis: ( y in x' & y is_>=_than x' )

now

per cases ( F' <> {} or F' = {} ) ;

suppose F' <> {} ; :: thesis: y in x'

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

end;

suppose F' = {} ; :: thesis: y in x'

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

end;

end;

end;

hence y in x' ; :: thesis: y is_>=_than x'

now

let b be Element of S; :: thesis: ( b in x' implies b <= y )
assume A5: b in x' ; :: thesis: b <= y

now

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

end;

then A7: F c= downarrow y by TARSKI:def 3;
downarrow y is Element of InIdS by YELLOW_2:43;
then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A7;
then b in downarrow y by A2, A5, SETFAM_1:def 1;
hence b <= y by WAYBEL_0:17; :: thesis: verum

end;

hence y is_>=_than x' 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 x' and
A9: y is_>=_than x' 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:28;
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 set st v in F holds
v in x by A8, TARSKI:def 1;
hence A10: F c= x by TARSKI:def 3; :: thesis: x = meet { Y where Y is Element of InIdS : F c= Y }
[#] S is Element of InIdS by YELLOW_2:43;
then A12: [#] S in { Y where Y is Element of InIdS : F c= Y } ;

now

let z be set ; :: 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 A13: 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 z' = z as Element of S by YELLOW_2:44;
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 and
A15: F c= Z1 ;
A16: Z1 is Ideal of S by YELLOW_2:43;
A17: y in F by TARSKI:def 1;
z' <= y by A9, A13, LATTICE3:def 9;
hence z in Z by A14, A15, A16, A17, 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 A18: 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 A18; :: thesis: verum

end;

end;

hence x = meet { Y where Y is Element of InIdS : F c= Y } by A12, 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;