let S be lower-bounded sup-Semilattice; :: thesis: for x being Element of (InclPoset (Ids S)) holds
( x is compact iff ex a being Element of S st x = downarrow a )
let x be Element of (InclPoset (Ids S)); :: thesis: ( x is compact iff ex a being Element of S st x = downarrow a )
thus ( x is compact implies ex a being Element of S st x = downarrow a ) :: thesis: ( ex a being Element of S st x = downarrow a implies x is compact )
proof
assume x is compact ; :: thesis: ex a being Element of S st x = downarrow a
then x is principal Ideal of S by Th11;
hence ex a being Element of S st x = downarrow a by WAYBEL_0:48; :: thesis: verum
end;
thus ( ex a being Element of S st x = downarrow a implies x is compact ) by WAYBEL_0:48, Th11; :: thesis: verum