for L being non empty with_suprema lower-bounded Poset holds
( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )