reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:17;
let A be Subset of REAL?; :: thesis: ( A = {REAL} implies A is closed )
reconsider B = B as Subset of R^1 ;
A1: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL \ NAT or x in ((REAL \ NAT) \/ {REAL}) \ {REAL} )
assume A2: x in REAL \ NAT ; :: thesis: x in ((REAL \ NAT) \/ {REAL}) \ {REAL}
then A3: x in REAL ;
A4: not x in {REAL}
proof
assume x in {REAL} ; :: thesis: contradiction
then A: x = REAL by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A, A3; :: thesis: verum
end;
x in (REAL \ NAT) \/ {REAL} by A2, XBOOLE_0:def 3;
hence x in ((REAL \ NAT) \/ {REAL}) \ {REAL} by A4, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((REAL \ NAT) \/ {REAL}) \ {REAL} or x in REAL \ NAT )
assume A5: x in ((REAL \ NAT) \/ {REAL}) \ {REAL} ; :: thesis: x in REAL \ NAT
then not x in {REAL} by XBOOLE_0:def 5;
hence x in REAL \ NAT by A5, XBOOLE_0:def 3; :: thesis: verum
end;
B misses NAT by XBOOLE_1:79;
then A6: B /\ NAT = {} ;
then reconsider C = B as Subset of REAL? by Th29;
assume A = {REAL} ; :: thesis: A is closed
then A7: C = A ` by A1, Def8;
B is open
proof
reconsider N = NAT as Subset of R^1 by TOPMETR:17, NUMBERS:19;
reconsider N = N as Subset of R^1 ;
( N is closed & N ` = B ) by Th10, TOPMETR:17;
hence B is open by TOPS_1:3; :: thesis: verum
end;
then C is open by A6, Th30;
hence A is closed by A7, TOPS_1:3; :: thesis: verum