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