let T1, T2 be non empty TopSpace; :: thesis: ( T1,T2 are_homeomorphic implies weight T2 c= weight T1 )
defpred S₁[ object ] means verum;
consider B1 being Basis of T1 such that
A1: card B1 = weight T1 by WAYBEL23:74;
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;
defpred S₂[ object ] means ( $1 in B1 & S₁[$1] );
A3: card { H₁(w) where w is Subset of T1 : S₂[w] } c= card B1 from BORSUK_2:sch 1();
consider B2 being Subset-Family of T2 such that
A4: B2 = { H₁(w) where w is Subset of T1 : S₂[w] } from LMOD_7:sch 5();
A5: 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 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 )
then A6: f " A is open by A2, 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;
then consider x being object such that
A9: x in dom f and
A10: f . x = p by FUNCT_1:def 3;
A11: x in f " A by A7, A9, A10, FUNCT_1:def 7;
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 A6, A11, 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:123;
hence ( a in B2 & p in a & a c= A ) by A4, A8, A9, A10, A12, FUNCT_1:77, FUNCT_1:def 6; :: thesis: verum

end;

A14: B1 c= the topology of T1 by TOPS_2:64;
B2 c= the topology of T2

proof

let x be object ; :: 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 A4;
w is open by A14, A16;
then H₁(w) is open by A2, TOPGRP_1:25;
hence x in the topology of T2 by A15; :: thesis: verum

end;

then reconsider B2 = B2 as Basis of T2 by A5, YELLOW_9:32;
weight T2 c= card B2 by WAYBEL23:73;
hence weight T2 c= weight T1 by A1, A4, A3; :: thesis: verum