Bottom L is compact by WAYBEL_3:15;
then reconsider c = Bottom L as Element of (CompactSublatt L) by WAYBEL_8:def 1;
take c ; :: according to YELLOW_0:def 4 :: thesis: c is_<=_than the carrier of (CompactSublatt L)
let b be Element of (CompactSublatt L); :: according to LATTICE3:def 8 :: thesis: ( not b in the carrier of (CompactSublatt L) or c <= b )
assume b in the carrier of (CompactSublatt L) ; :: thesis: c <= b
reconsider x = b as Element of L by YELLOW_0:58;
Bottom L <= x by YELLOW_0:44;
hence c <= b by YELLOW_0:60; :: thesis: verum