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: f is being_homeomorphism
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 A1, TOPS_2:def 4;
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 A4, SETFAM_1:def 9;
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 A2, A4, A7, FUNCT_2:def 10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
x = f " (f .: A) by a3, FUNCT_1:85, A7, A8
.= A by A1, A9, FUNCT_1:94 ;
hence x in K by A8; :: thesis: verum

end;

hence ( X c= K & X is finite ) by A4, TARSKI:def 3; :: thesis: V = Intersect X
consider B being object such that
A10: B in Y by A5, XBOOLE_0:def 1;
reconsider B = B as Subset of T by A10;
g .: B in X by A10, FUNCT_2:def 10;
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 A1, FUNCT_2:def 3;

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 A12, FUNCT_2:def 10;
x = f .: (f " B) by a3, FUNCT_1:85, A12, A13
.= B by A11, FUNCT_1:77 ;
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 A14, FUNCT_2:def 10;
f .: (g .: B) = f .: (f " B) by a3, FUNCT_1:85
.= B by A11, FUNCT_1:77 ;
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 A4, SETFAM_1:def 9;
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 XBOOLE_1:2, STRUCT_0:def 3;
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 A16, A1, FUNCT_2:def 3 ; :: 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 A17, CANTOR_1:def 3;

per cases ( X <> {} or X = {} ) ;

suppose A19: X <> {} ; :: thesis: W in L0

then A20: V = meet X by A18, SETFAM_1:def 9;
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 A2, FUNCT_2:def 10, A18; :: thesis: verum

end;

thus Y is finite by A18; :: thesis: W = Intersect Y
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 A19, XBOOLE_0:def 1;
reconsider A = A as Subset of S by A25;
f .: A in f .: X by A25, FUNCT_2:def 10;
hence W = Intersect Y by A24, SETFAM_1:def 9; :: 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 A18, SETFAM_1:def 9;
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 A17, A26, FUNCT_2:def 1
.= rng f by RELAT_1:113
.= the carrier of T by A1, FUNCT_2:def 3
.= Intersect the empty Subset-Family of T by SETFAM_1:def 9 ;
hence W in L0 by B1, CANTOR_1:def 3; :: thesis: verum

end;

end;

end;

then f .: K0 = L0 by FUNCT_2:def 10;
hence f is being_homeomorphism by A1, Th47; :: thesis: verum