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;

Bottom L in C by WAYBEL_8:3;

hence the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Def8; :: thesis: verum

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)

then reconsider C = C as CLbasis of L by Def7;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;x = sup (compactbelow x) by WAYBEL_8:def 3;

hence x = sup ((waybelow x) /\ C) by Th1; :: thesis: verum

Bottom L in C by WAYBEL_8:3;

hence the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Def8; :: thesis: verum