let T be non empty T_0 TopSpace; :: thesis: for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds
weight T = CLweight L1
let L1 be lower-bounded continuous sup-Semilattice; :: thesis: ( InclPoset the topology of T = L1 & T is infinite implies weight T = CLweight L1 )
assume that
A1: InclPoset the topology of T = L1 and
A2: T is infinite ; :: thesis: weight T = CLweight L1
A3: { (card B1) where B1 is Basis of T : verum } c= { (card B1) where B1 is with_bottom CLbasis of L1 : verum }

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { (card B1) where B1 is Basis of T : verum } or b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } )
assume b in { (card B1) where B1 is Basis of T : verum } ; :: thesis: b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum }
then consider B2 being Basis of T such that
A4: b = card B2 ;
B2 c= the topology of T by TOPS_2:64;
then reconsider B3 = B2 as Subset of L1 by A1, YELLOW_1:1;
B2 is infinite by A2, YELLOW15:30;
then A5: card B2 = card (finsups B3) by YELLOW15:27;
finsups B3 is with_bottom CLbasis of L1 by A1, Th5;
hence b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A4, A5; :: thesis: verum

end;

{ (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= { (card B1) where B1 is Basis of T : verum }

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } or b in { (card B1) where B1 is Basis of T : verum } )
assume b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; :: thesis: b in { (card B1) where B1 is Basis of T : verum }
then consider B2 being with_bottom CLbasis of L1 such that
A6: b = card B2 ;
B2 is Basis of T by A1, Th4;
hence b in { (card B1) where B1 is Basis of T : verum } by A6; :: thesis: verum

end;

then { (card B1) where B1 is Basis of T : verum } = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A3, XBOOLE_0:def 10;
hence weight T = CLweight L1 by WAYBEL23:def 5; :: thesis: verum