let A be Subset of REAL? ; :: thesis: ( A = {REAL } implies A is closed )
assume A1: A = {REAL } ; :: thesis: A is closed
reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:24;
reconsider B = B as Subset of R^1 ;
A2: B is open

proof

reconsider N = NAT as Subset of R^1 by TOPMETR:24;
reconsider N = N as Subset of R^1 ;
A3: N is closed by Th10;
N ` = B by TOPMETR:24;
hence B is open by A3, TOPS_1:29; :: thesis: verum

end;

B misses NAT by XBOOLE_1:79;
then A4: B /\ NAT = {} by XBOOLE_0:def 7;
then reconsider C = B as Subset of REAL? by Th32;
A5: C is open by A2, A4, Th33;
REAL \ NAT = ((REAL \ NAT ) \/ {REAL }) \ {REAL }

proof

thus REAL \ NAT c= ((REAL \ NAT ) \/ {REAL }) \ {REAL } :: according to XBOOLE_0:def 10 :: thesis: ((REAL \ NAT ) \/ {REAL }) \ {REAL } c= REAL \ NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL \ NAT or x in ((REAL \ NAT ) \/ {REAL }) \ {REAL } )
assume A6: x in REAL \ NAT ; :: thesis: x in ((REAL \ NAT ) \/ {REAL }) \ {REAL }
then A7: x in REAL ;
A8: not x in {REAL }

proof

assume x in {REAL } ; :: thesis: contradiction
then x = REAL by TARSKI:def 1;
hence contradiction by A7; :: thesis: verum

end;

x in (REAL \ NAT ) \/ {REAL } by A6, XBOOLE_0:def 3;
hence x in ((REAL \ NAT ) \/ {REAL }) \ {REAL } by A8, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((REAL \ NAT ) \/ {REAL }) \ {REAL } or x in REAL \ NAT )
assume x in ((REAL \ NAT ) \/ {REAL }) \ {REAL } ; :: thesis: x in REAL \ NAT
then ( x in (REAL \ NAT ) \/ {REAL } & not x in {REAL } ) by XBOOLE_0:def 5;
hence x in REAL \ NAT by XBOOLE_0:def 3; :: thesis: verum

end;

then C = A ` by A1, Def7;
hence A is closed by A5, TOPS_1:29; :: thesis: verum