let X, Y be non empty strict TopSpace; :: thesis: ( the carrier of X = (REAL \ NAT ) \/ {REAL } & ex f being Function of R^1 ,X st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of X holds
( A is closed iff f " A is closed ) ) ) & the carrier of Y = (REAL \ NAT ) \/ {REAL } & ex f being Function of R^1 ,Y st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of Y holds
( A is closed iff f " A is closed ) ) ) implies X = Y )
assume that
A5: ( the carrier of X = (REAL \ NAT ) \/ {REAL } & ex f being Function of R^1 ,X st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of X holds
( A is closed iff f " A is closed ) ) ) ) and
A6: ( the carrier of Y = (REAL \ NAT ) \/ {REAL } & ex f being Function of R^1 ,Y st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of Y holds
( A is closed iff f " A is closed ) ) ) ) ; :: thesis: X = Y
consider f being Function of R^1 ,X such that
A7: f = (id REAL ) +* (NAT --> REAL ) and
A8: for A being Subset of X holds
( A is closed iff f " A is closed ) by A5;
consider g being Function of R^1 ,Y such that
A9: g = (id REAL ) +* (NAT --> REAL ) and
A10: for A being Subset of Y holds
( A is closed iff g " A is closed ) by A6;
the topology of X = the topology of Y

proof

thus the topology of X c= the topology of Y :: according to XBOOLE_0:def 10 :: thesis: the topology of Y c= the topology of X

proof

let V be set ; :: according to TARSKI:def 3 :: thesis: ( not V in the topology of X or V in the topology of Y )
assume A11: V in the topology of X ; :: thesis: V in the topology of Y
then reconsider V1 = V as Subset of X ;
reconsider V1 = V1 as Subset of X ;
V1 is open by A11, PRE_TOPC:def 5;
then ([#] X) \ V1 is closed by Lm3;
then A12: g " (([#] X) \ V1) is closed by A7, A8, A9;
reconsider V2 = V as Subset of Y by A5, A6, A11;
reconsider V2 = V2 as Subset of Y ;
([#] Y) \ V2 is closed by A5, A6, A10, A12;
then V2 is open by Lm3;
hence V in the topology of Y by PRE_TOPC:def 5; :: thesis: verum

end;

thus the topology of Y c= the topology of X :: thesis: verum

proof

let V be set ; :: according to TARSKI:def 3 :: thesis: ( not V in the topology of Y or V in the topology of X )
assume A13: V in the topology of Y ; :: thesis: V in the topology of X
then reconsider V1 = V as Subset of Y ;
reconsider V1 = V1 as Subset of Y ;
V1 is open by A13, PRE_TOPC:def 5;
then ([#] Y) \ V1 is closed by Lm3;
then A14: f " (([#] Y) \ V1) is closed by A7, A9, A10;
reconsider V2 = V as Subset of X by A5, A6, A13;
reconsider V2 = V2 as Subset of X ;
([#] X) \ V2 is closed by A5, A6, A8, A14;
then V2 is open by Lm3;
hence V in the topology of X by PRE_TOPC:def 5; :: thesis: verum

end;

end;

hence X = Y by A5, A6; :: thesis: verum