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

assume compactbelow x is principal Ideal of (CompactSublatt L) ; :: thesis:
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:

end;

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

reconsider I = compactbelow x as non empty Subset of (CompactSublatt L) by Th2;
assume A4: x is compact ; :: thesis:
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;

let y, z be Element of (CompactSublatt L); :: thesis:
reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58;
assume ( y in I & z <= y ) ; :: thesis:
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:

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:

end;