let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds
CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
let B1 be with_bottom CLbasis of L1; :: thesis: ( card B1 = CLweight L1 implies CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) )
assume A1: card B1 = CLweight L1 ; :: thesis: CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
A2: card the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B1)))) = card the carrier of (subrelstr B1) by Th26, WAYBEL23:69;
thus CLweight (InclPoset (Ids (subrelstr B1))) = card the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B1)))) by Th3
.= CLweight L1 by A1, A2, YELLOW_0:def 15 ; :: thesis: verum