theorem :: WAYBEL23:69

for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic