let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds
f is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L implies f is being_homeomorphism )
assume A1: f is bijective ; :: thesis: ( for K being Basis of S
for L being Basis of T holds not f .: K = L or f is being_homeomorphism )

given K being Basis of S, L being Basis of T such that A2: f .: K = L ; :: thesis:
for W being Subset of T st W in L holds
f " W is open
proof
let W be Subset of T; :: thesis: ( W in L implies f " W is open )
assume W in L ; :: thesis: f " W is open
then consider V being Subset of S such that
A3: ( V in K & W = f .: V ) by ;
dom f = the carrier of S by FUNCT_2:def 1;
then V = f " W by ;
hence f " W is open by ; :: thesis: verum
end;
then A4: f is continuous by YELLOW_9:34;
for V being Subset of S st V in K holds
f .: V is open
proof
let V be Subset of S; :: thesis: ( V in K implies f .: V is open )
assume V in K ; :: thesis: f .: V is open
then f .: V in f .: K by FUNCT_2:def 10;
hence f .: V is open by ; :: thesis: verum
end;
then f is open by Th45;
then A5: f " is continuous by ;
A6: rng f = the carrier of T by
.= [#] T by STRUCT_0:def 3 ;
dom f = the carrier of S by FUNCT_2:def 1
.= [#] S by STRUCT_0:def 3 ;
hence f is being_homeomorphism by ; :: thesis: verum