let L be lower-bounded algebraic LATTICE; :: thesis: the carrier of (CompactSublatt L) is with_bottom CLbasis of L
reconsider C = the carrier of (CompactSublatt L) as join-closed Subset of L by Th43;
now :: thesis: for x being Element of L holds x = sup ((waybelow x) /\ C)
let x be Element of L; :: thesis: x = sup ((waybelow x) /\ C)
x = sup (compactbelow x) by WAYBEL_8:def 3;
hence x = sup ((waybelow x) /\ C) by Th1; :: thesis: verum
end;
then reconsider C = C as CLbasis of L by Def7;
Bottom L in C by WAYBEL_8:3;
hence the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Def8; :: thesis: verum