reconsider X = (REAL \ NAT ) \/ {REAL } as non empty set ;
set f = (id REAL ) +* (NAT --> REAL );
REAL \/ NAT = REAL by XBOOLE_1:12;
then A1: dom ((id REAL ) +* (NAT --> REAL )) = the carrier of R^1 by Th15, TOPMETR:24;
rng ((id REAL ) +* (NAT --> REAL )) c= (REAL \ NAT ) \/ {REAL } by Th16;
then reconsider f = (id REAL ) +* (NAT --> REAL ) as Function of the carrier of R^1 ,X by A1, FUNCT_2:4;
set O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } ;
{ (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } c= bool X

proof

let B be set ; :: according to TARSKI:def 3 :: thesis: ( not B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } or B in bool X )
assume B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } ; :: thesis: B in bool X
then consider A being Subset of X such that
A2: ( B = X \ A & ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) ) ;
thus B in bool X by A2; :: thesis: verum

end;

then reconsider O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( fA = f " A & fA is closed ) } as Subset-Family of X ;
set T = TopStruct(# X,O #);
reconsider f = f as Function of R^1 ,TopStruct(# X,O #) ;
A3: for A being Subset of TopStruct(# X,O #) holds
( A is closed iff f " A is closed )

proof

let A be Subset of TopStruct(# X,O #); :: thesis: ( A is closed iff f " A is closed )
thus ( A is closed implies f " A is closed ) :: thesis: ( f " A is closed implies A is closed )

proof

assume A is closed ; :: thesis: f " A is closed
then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 6;
then ([#] TopStruct(# X,O #)) \ A in the topology of TopStruct(# X,O #) by PRE_TOPC:def 5;
then consider B being Subset of X such that
A4: ( X \ B = ([#] TopStruct(# X,O #)) \ A & ex fA being Subset of R^1 st
( fA = f " B & fA is closed ) ) ;
B = ([#] TopStruct(# X,O #)) \ (([#] TopStruct(# X,O #)) \ A) by A4, PRE_TOPC:22;
hence f " A is closed by A4, PRE_TOPC:22; :: thesis: verum

end;

assume f " A is closed ; :: thesis: A is closed
then X \ A in O ;
then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 5;
hence A is closed by PRE_TOPC:def 6; :: thesis: verum

end;

then reconsider T = TopStruct(# X,O #) as non empty strict TopSpace by Th6;
take T ; :: thesis: ( the carrier of T = (REAL \ NAT ) \/ {REAL } & ex f being Function of R^1 ,T st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) ) )
thus the carrier of T = (REAL \ NAT ) \/ {REAL } ; :: thesis: ex f being Function of R^1 ,T st
( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) )
reconsider f = f as Function of R^1 ,T ;
take f ; :: thesis: ( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) )
thus ( f = (id REAL ) +* (NAT --> REAL ) & ( for A being Subset of T holds
( A is closed iff f " A is closed ) ) ) by A3; :: thesis: verum