let L be lower-bounded sup-Semilattice; :: thesis: CompactSublatt L is lower-bounded sup-Semilattice
ex x being Element of (CompactSublatt L) st x is_<=_than the carrier of (CompactSublatt L)
proof
reconsider x = Bottom L as Element of (CompactSublatt L) by WAYBEL_8:3;
take x ; :: thesis: x is_<=_than the carrier of (CompactSublatt L)
now :: thesis: for a being Element of (CompactSublatt L) st a in the carrier of (CompactSublatt L) holds
x <= a
let a be Element of (CompactSublatt L); :: thesis: ( a in the carrier of (CompactSublatt L) implies x <= a )
A1: the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;
assume a in the carrier of (CompactSublatt L) ; :: thesis: x <= a
reconsider a9 = a as Element of L by A1;
Bottom L <= a9 by YELLOW_0:44;
hence x <= a by YELLOW_0:60; :: thesis: verum
end;
hence x is_<=_than the carrier of (CompactSublatt L) by LATTICE3:def 8; :: thesis: verum
end;
hence CompactSublatt L is lower-bounded sup-Semilattice by YELLOW_0:def 4; :: thesis: verum