theorem :: WAYBEL31:27

for L1 being lower-bounded continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds
CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))