let T1, T2 be TopSpace; :: thesis: ( T1,T2 are_homeomorphic implies weight T1 = weight T2 )
assume A1: T1,T2 are_homeomorphic ; :: thesis: weight T1 = weight T2

per cases ( [#] T1 = {} or [#] T2 = {} or ( not T1 is empty & not T2 is empty ) ) ;

suppose A2: ( [#] T1 = {} or [#] T2 = {} ) ; :: thesis: weight T1 = weight T2

A3: ( T1 is empty iff T2 is empty ) by A1, YELLOW14:18;
then weight T1 = 0 by A2, Lm3;
hence weight T1 = weight T2 by A2, A3, Lm3; :: thesis: verum

end;

suppose ( not T1 is empty & not T2 is empty ) ; :: thesis: weight T1 = weight T2

then ( weight T2 c= weight T1 & weight T1 c= weight T2 ) by A1, Lm2;
hence weight T1 = weight T2 ; :: thesis: verum

end;

end;