let T1, T2 be TopSpace; :: thesis: ( T1 is second-countable & T1,T2 are_homeomorphic implies T2 is second-countable )

assume T1 is second-countable ; :: thesis: ( not T1,T2 are_homeomorphic or T2 is second-countable )

then A1: weight T1 c= omega by WAYBEL23:def 6;

assume T1,T2 are_homeomorphic ; :: thesis: T2 is second-countable

then weight T1 = weight T2 by METRIZTS:4;

hence T2 is second-countable by A1, WAYBEL23:def 6; :: thesis: verum

assume T1 is second-countable ; :: thesis: ( not T1,T2 are_homeomorphic or T2 is second-countable )

then A1: weight T1 c= omega by WAYBEL23:def 6;

assume T1,T2 are_homeomorphic ; :: thesis: T2 is second-countable

then weight T1 = weight T2 by METRIZTS:4;

hence T2 is second-countable by A1, WAYBEL23:def 6; :: thesis: verum