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 y9 = y as Element of L by YELLOW_0:58;
compactbelow x is Subset of (CompactSublatt L) by Th2;
then y9 is_>=_than compactbelow x by A2, YELLOW_0:62;
then y9 >= sup (compactbelow x) by YELLOW_0:32;
then A3: x <= y9 by WAYBEL_8:def 3;
( y9 <= x & y9 is compact ) by A1, WAYBEL_8:4;
hence x is compact by A3, ORDERS_2:2; :: thesis: verum

end;

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

proof

reconsider I = compactbelow x as non empty Subset of (CompactSublatt L) by Th2;
assume A4: x is compact ; :: thesis: compactbelow x is principal Ideal of (CompactSublatt L)
then reconsider x9 = x as Element of (CompactSublatt L) by WAYBEL_8:def 1;
compactbelow x is non empty directed Subset of L by WAYBEL_8:def 4;
then reconsider I = I as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23;

now :: thesis: for y, z being Element of (CompactSublatt L) st y in I & z <= y holds
z in I

let y, z be Element of (CompactSublatt L); :: thesis: ( y in I & z <= y implies z in I )
reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58;
assume ( y in I & z <= y ) ; :: thesis: z in I
then ( y9 <= x & z9 <= y9 ) by WAYBEL_8:4, YELLOW_0:59;
then A5: z9 <= x by ORDERS_2:3;
z9 is compact by WAYBEL_8:def 1;
hence z in I by A5, WAYBEL_8:4; :: thesis: verum

end;

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

end;