let X, Y be non empty TopSpace; :: thesis: for f being continuous Function of X,Y st f is one-to-one & f is onto holds
( f is being_homeomorphism iff f is closed )
let f be continuous Function of X,Y; :: thesis: ( f is one-to-one & f is onto implies ( f is being_homeomorphism iff f is closed ) )
assume A1: ( f is one-to-one & f is onto ) ; :: thesis: ( f is being_homeomorphism iff f is closed )

hereby :: thesis: ( f is closed implies f is being_homeomorphism )

assume A2: f is being_homeomorphism ; :: thesis: f is closed
thus f is closed :: thesis: verum

proof

let A be Subset of X; :: according to JORDAN24:def 4 :: thesis: ( A is closed implies f .: A is closed )
thus ( A is closed implies f .: A is closed ) by A2, TOPS_2:72; :: thesis: verum

end;

end;

assume A3: for A being Subset of X st A is closed holds
f .: A is closed ; :: according to JORDAN24:def 4 :: thesis: f is being_homeomorphism
A4: ( dom f = the carrier of X & rng f = the carrier of Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
A5: ( [#] X = the carrier of X & [#] Y = the carrier of Y ) ;

now

let A be Subset of X; :: thesis: ( f .: A is closed implies A is closed )
assume f .: A is closed ; :: thesis: A is closed
then f " (f .: A) is closed by PRE_TOPC:def 12;
hence A is closed by A1, A4, FUNCT_1:164; :: thesis: verum

end;

hence f is being_homeomorphism by A1, A3, A4, A5, TOPS_2:72; :: thesis: verum