let L be lower-bounded sup-Semilattice; :: thesis: InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L)
CompactSublatt L is lower-bounded sup-Semilattice by Th15;
hence InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) by Th8; :: thesis: verum