let L be lower-bounded algebraic sup-Semilattice; :: thesis: for x being Element of L holds
( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
let x be Element of L; :: thesis: ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
thus ( compactbelow x is principal Ideal of (CompactSublatt L) implies x is compact ) :: thesis: ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) )

proof

assume compactbelow x is principal Ideal of (CompactSublatt L) ; :: thesis: x is compact
then consider y being Element of (CompactSublatt L) such that
A1: y in compactbelow x and
A2: y is_>=_than compactbelow x by WAYBEL_0:def 21;
reconsider y' = y as Element of L by YELLOW_0:59;
compactbelow x is Subset of (CompactSublatt L) by Th2;
then y' is_>=_than compactbelow x by A2, YELLOW_0:63;
then y' >= sup (compactbelow x) by YELLOW_0:32;
then A3: x <= y' by WAYBEL_8:def 3;
( y' <= x & y' is compact ) by A1, WAYBEL_8:4;
hence x is compact by A3, ORDERS_2:25; :: thesis: verum

end;

thus ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) ) :: thesis: verum

proof

assume A4: x is compact ; :: thesis: compactbelow x is principal Ideal of (CompactSublatt L)
A5: compactbelow x is non empty directed Subset of L by WAYBEL_8:def 4;
reconsider I = compactbelow x as non empty Subset of (CompactSublatt L) by Th2;
reconsider I = I as non empty directed Subset of (CompactSublatt L) by A5, WAYBEL10:24;

now

let y, z be Element of (CompactSublatt L); :: thesis: ( y in I & z <= y implies z in I )
reconsider y' = y, z' = z as Element of L by YELLOW_0:59;
assume A6: ( y in I & z <= y ) ; :: thesis: z in I
then A7: y' <= x by WAYBEL_8:4;
z' <= y' by A6, YELLOW_0:60;
then A8: z' <= x by A7, ORDERS_2:26;
z' is compact by WAYBEL_8:def 1;
hence z in I by A8, WAYBEL_8:4; :: thesis: verum

end;

then reconsider I = I as Ideal of (CompactSublatt L) by WAYBEL_0:def 19;
reconsider x' = x as Element of (CompactSublatt L) by A4, WAYBEL_8:def 1;
x <= x ;
then A9: x' in I by A4, WAYBEL_8:4;
sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
then x is_>=_than I by WAYBEL_8:def 3;
then x' is_>=_than I by YELLOW_0:62;
hence compactbelow x is principal Ideal of (CompactSublatt L) by A9, WAYBEL_0:def 21; :: thesis: verum

end;