let S be lower-bounded sup-Semilattice; :: thesis: for x being Element of holds
( x is compact iff ex a being Element of st x = downarrow a )
let x be Element of ; :: thesis: ( x is compact iff ex a being Element of st x = downarrow a )
thus ( x is compact implies ex a being Element of st x = downarrow a ) :: thesis: ( ex a being Element of st x = downarrow a implies x is compact )

proof

assume x is compact ; :: thesis: ex a being Element of st x = downarrow a
then x is principal Ideal of S by Th11;
hence ex a being Element of st x = downarrow a by WAYBEL_0:48; :: thesis: verum

end;

thus ( ex a being Element of st x = downarrow a implies x is compact ) :: thesis: verum

proof

assume ex a being Element of st x = downarrow a ; :: thesis: x is compact
then x is principal Ideal of S by WAYBEL_0:48;
hence x is compact by Th11; :: thesis: verum

end;