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}

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

hence A is closed by A7, TOPS_1:3; :: thesis: verum

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

B misses NAT
by XBOOLE_1:79;
thus
REAL \ NAT c= ((REAL \ NAT) \/ {REAL}) \ {REAL}
:: according to XBOOLE_0:def 10 :: thesis: ((REAL \ NAT) \/ {REAL}) \ {REAL} c= 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((REAL \ NAT) \/ {REAL}) \ {REAL} or x in REAL \ NAT )
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}

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

end;assume A2: x in REAL \ NAT ; :: thesis: x in ((REAL \ NAT) \/ {REAL}) \ {REAL}

then A3: x in REAL ;

A4: not x in {REAL}

proof

x in (REAL \ NAT) \/ {REAL}
by A2, XBOOLE_0:def 3;
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;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

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

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

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

then
C is open
by A6, Th30;
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;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

hence A is closed by A7, TOPS_1:3; :: thesis: verum