reconsider B = REAL \ NAT as Subset of R^1 by TOPMETR:17;
let A be Subset of REAL?; :: thesis: ( A = implies A is closed )
reconsider B = B as Subset of R^1 ;
A1: REAL \ NAT = (() \/ ) \
proof
thus REAL \ NAT c= (() \/ ) \ :: according to XBOOLE_0:def 10 :: thesis:
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL \ NAT or x in (() \/ ) \ )
assume A2: x in REAL \ NAT ; :: thesis: x in (() \/ ) \
then A3: x in REAL ;
A4: not x in
proof
assume x in ; :: 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 () \/ by ;
hence x in (() \/ ) \ by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (() \/ ) \ or x in REAL \ NAT )
assume A5: x in (() \/ ) \ ; :: thesis:
then not x in by XBOOLE_0:def 5;
hence x in REAL \ NAT by ; :: 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 = ; :: thesis: A is closed
then A7: C = A ` by ;
B is open
proof
reconsider N = NAT as Subset of R^1 by ;
reconsider N = N as Subset of R^1 ;
( N is closed & N ` = B ) by ;
hence B is open by TOPS_1:3; :: thesis: verum
end;
then C is open by ;
hence A is closed by ; :: thesis: verum