let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is bijective & ex K being prebasis of S ex L being prebasis 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 prebasis of S ex L being prebasis of T st f .: K = L implies f is being_homeomorphism )
assume A1: f is bijective ; :: thesis: ( for K being prebasis of S
for L being prebasis of T holds not f .: K = L or f is being_homeomorphism )

given K being prebasis of S, L being prebasis of T such that A2: f .: K = L ; :: thesis:
reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
reconsider g = f " as Function of T,S ;
reconsider f0 = f as one-to-one Function by A1;
a3: f0 " = g by ;
for W being Subset of T holds
( W in L0 iff ex V being Subset of S st
( V in K0 & f .: V = W ) )
proof
let W be Subset of T; :: thesis: ( W in L0 iff ex V being Subset of S st
( V in K0 & f .: V = W ) )

thus ( W in L0 implies ex V being Subset of S st
( V in K0 & f .: V = W ) ) :: thesis: ( ex V being Subset of S st
( V in K0 & f .: V = W ) implies W in L0 )
proof
assume W in L0 ; :: thesis: ex V being Subset of S st
( V in K0 & f .: V = W )

then consider Y being Subset-Family of T such that
A4: ( Y c= L & Y is finite & W = Intersect Y ) by CANTOR_1:def 3;
per cases ( Y <> {} or Y = {} ) ;
suppose A5: Y <> {} ; :: thesis: ex V being Subset of S st
( V in K0 & f .: V = W )

then A6: W = meet Y by ;
reconsider X = g .: Y as Subset-Family of S ;
reconsider V = meet X as Subset of S ;
take V ; :: thesis: ( V in K0 & f .: V = W )
ex Z being Subset-Family of S st
( Z c= K & Z is finite & V = Intersect Z )
proof
take X ; :: thesis: ( X c= K & X is finite & V = Intersect X )
for x being object st x in X holds
x in K
proof
let x be object ; :: thesis: ( x in X implies x in K )
assume x in X ; :: thesis: x in K
then consider B being Subset of T such that
A7: ( B in Y & x = g .: B ) by FUNCT_2:def 10;
consider A being Subset of S such that
A8: ( A in K & B = f .: A ) by ;
A9: dom f = the carrier of S by FUNCT_2:def 1;
x = f " (f .: A) by
.= A by ;
hence x in K by A8; :: thesis: verum
end;
hence ( X c= K & X is finite ) by ; :: thesis:
consider B being object such that
A10: B in Y by ;
reconsider B = B as Subset of T by A10;
g .: B in X by ;
hence V = Intersect X by SETFAM_1:def 9; :: thesis: verum
end;
hence V in K0 by CANTOR_1:def 3; :: thesis: f .: V = W
set Z = { (f .: A) where A is Subset of S : A in X } ;
for x being object holds
( x in { (f .: A) where A is Subset of S : A in X } iff x in Y )
proof
let x be object ; :: thesis: ( x in { (f .: A) where A is Subset of S : A in X } iff x in Y )
A11: rng f = the carrier of T by ;
hereby :: thesis: ( x in Y implies x in { (f .: A) where A is Subset of S : A in X } )
assume x in { (f .: A) where A is Subset of S : A in X } ; :: thesis: x in Y
then consider A being Subset of S such that
A12: ( f .: A = x & A in X ) ;
consider B being Subset of T such that
A13: ( B in Y & A = g .: B ) by ;
x = f .: (f " B) by
.= B by ;
hence x in Y by A13; :: thesis: verum
end;
assume A14: x in Y ; :: thesis: x in { (f .: A) where A is Subset of S : A in X }
then reconsider B = x as Subset of T ;
A15: g .: B in X by ;
f .: (g .: B) = f .: (f " B) by
.= B by ;
hence x in { (f .: A) where A is Subset of S : A in X } by A15; :: thesis: verum
end;
then { (f .: A) where A is Subset of S : A in X } = Y by TARSKI:2;
hence f .: V = W by A1, A6, Th4; :: thesis: verum
end;
suppose Y = {} ; :: thesis: ex V being Subset of S st
( V in K0 & f .: V = W )

then A16: W = the carrier of T by ;
set V = [#] S;
take [#] S ; :: thesis: ( [#] S in K0 & f .: ([#] S) = W )
set Z = the empty Subset-Family of S;
Intersect the empty Subset-Family of S = the carrier of S by SETFAM_1:def 9;
then ( the empty Subset-Family of S c= K & the empty Subset-Family of S is finite & [#] S = Intersect the empty Subset-Family of S ) by ;
hence [#] S in K0 by CANTOR_1:def 3; :: thesis: f .: ([#] S) = W
thus f .: ([#] S) = f .: the carrier of S by STRUCT_0:def 3
.= f .: (dom f) by FUNCT_2:def 1
.= rng f by RELAT_1:113
.= W by ; :: thesis: verum
end;
end;
end;
given V being Subset of S such that A17: ( V in K0 & f .: V = W ) ; :: thesis: W in L0
consider X being Subset-Family of S such that
A18: ( X c= K & X is finite & V = Intersect X ) by ;
per cases ( X <> {} or X = {} ) ;
suppose A19: X <> {} ; :: thesis: W in L0
then A20: V = meet X by ;
ex Y being Subset-Family of T st
( Y c= L & Y is finite & W = Intersect Y )
proof
reconsider Y = f .: X as Subset-Family of T ;
take Y ; :: thesis: ( Y c= L & Y is finite & W = Intersect Y )
thus Y c= L :: thesis: ( Y is finite & W = Intersect Y )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in L )
assume x in Y ; :: thesis: x in L
then ex A being Subset of S st
( A in X & f .: A = x ) by FUNCT_2:def 10;
hence x in L by ; :: thesis: verum
end;
thus Y is finite by A18; :: thesis:
set Z = { (f .: A) where A is Subset of S : A in X } ;
for x being object holds
( x in Y iff x in { (f .: A) where A is Subset of S : A in X } )
proof
let x be object ; :: thesis: ( x in Y iff x in { (f .: A) where A is Subset of S : A in X } )
hereby :: thesis: ( x in { (f .: A) where A is Subset of S : A in X } implies x in Y )
assume x in Y ; :: thesis: x in { (f .: A) where A is Subset of S : A in X }
then ex A being Subset of S st
( A in X & f .: A = x ) by FUNCT_2:def 10;
hence x in { (f .: A) where A is Subset of S : A in X } ; :: thesis: verum
end;
assume x in { (f .: A) where A is Subset of S : A in X } ; :: thesis: x in Y
then ex A being Subset of S st
( f .: A = x & A in X ) ;
hence x in Y by FUNCT_2:def 10; :: thesis: verum
end;
then Y = { (f .: A) where A is Subset of S : A in X } by TARSKI:2;
then A24: meet Y = W by A1, A17, A20, Th4;
consider A being object such that
A25: A in X by ;
reconsider A = A as Subset of S by A25;
f .: A in f .: X by ;
hence W = Intersect Y by ; :: thesis: verum
end;
hence W in L0 by CANTOR_1:def 3; :: thesis: verum
end;
suppose X = {} ; :: thesis: W in L0
then A26: V = the carrier of S by ;
set Y = the empty Subset-Family of T;
B1: ( the empty Subset-Family of T c= L & the empty Subset-Family of T is finite ) by XBOOLE_1:2;
W = f .: (dom f) by
.= rng f by RELAT_1:113
.= the carrier of T by
.= Intersect the empty Subset-Family of T by SETFAM_1:def 9 ;
hence W in L0 by ; :: thesis: verum
end;
end;
end;
then f .: K0 = L0 by FUNCT_2:def 10;
hence f is being_homeomorphism by ; :: thesis: verum