defpred S₁[ set ] means verum;
let T1, T2 be non empty TopSpace; :: thesis: ( T1,T2 are_homeomorphic implies weight T2 c= weight T1 )
consider B1 being Basis of T1 such that
A1: card B1 = weight T1 by WAYBEL23:75;
defpred S₂[ set ] means ( $1 in B1 & S₁[$1] );
assume T1,T2 are_homeomorphic ; :: thesis: weight T2 c= weight T1
then consider f being Function of T1,T2 such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
deffunc H₁( Subset of T1) -> Element of bool the carrier of T2 = f .: $1;
consider B2 being Subset-Family of T2 such that
A3: B2 = { H₁(w) where w is Subset of T1 : S₂[w] } from LMOD_7:sch 5();
A4: for A being Subset of T2 st A is open holds
for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )

proof

let A be Subset of T2; :: thesis: ( A is open implies for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A ) )
assume A5: A is open ; :: thesis: for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
A6: f " A is open by A2, A5, TOPGRP_1:26;
let p be Point of T2; :: thesis: ( p in A implies ex a being Subset of T2 st
( a in B2 & p in a & a c= A ) )
assume A7: p in A ; :: thesis: ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
A8: rng f = [#] T2 by A2, TOPGRP_1:25;
then consider x being set such that
A9: x in dom f and
A10: f . x = p by FUNCT_1:def 5;
A11: x in f " A by A7, A9, A10, FUNCT_1:def 13;
reconsider x = x as Point of T1 by A9;
consider a1 being Subset of T1 such that
A12: ( a1 in B1 & x in a1 ) and
A13: a1 c= f " A by A11, A6, YELLOW_9:31;
take a = H₁(a1); :: thesis: ( a in B2 & p in a & a c= A )
a c= f .: (f " A) by A13, RELAT_1:156;
hence ( a in B2 & p in a & a c= A ) by A3, A8, A9, A10, A12, FUNCT_1:147, FUNCT_1:def 12; :: thesis: verum

end;

A14: B1 c= the topology of T1 by CANTOR_1:def 2;
B2 c= the topology of T2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in the topology of T2 )
assume x in B2 ; :: thesis: x in the topology of T2
then consider w being Subset of T1 such that
A15: x = H₁(w) and
A16: S₂[w] by A3;
w is open by A14, A16, PRE_TOPC:def 5;
then H₁(w) is open by A2, TOPGRP_1:25;
hence x in the topology of T2 by A15, PRE_TOPC:def 5; :: thesis: verum

end;

then reconsider B2 = B2 as Basis of T2 by A4, YELLOW_9:32;
A17: card { H₁(w) where w is Subset of T1 : S₂[w] } c= card B1 from BORSUK_2:sch 1();
weight T2 c= card B2 by WAYBEL23:74;
hence weight T2 c= weight T1 by A1, A3, A17, XBOOLE_1:1; :: thesis: verum