let A be Subset of R^1 ; :: thesis: for B being Subset of REAL? st A = B holds
( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
let B be Subset of REAL? ; :: thesis: ( A = B implies ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) ) )
assume A1: A = B ; :: thesis: ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
consider f being Function of R^1 ,REAL? such that
A2: f = (id REAL ) +* (NAT --> REAL ) and
A3: for A being Subset of REAL? holds
( A is closed iff f " A is closed ) by Def7;
A4: ( NAT /\ A = {} & not REAL in B implies f " (B ` ) = A ` )

proof

assume A5: ( NAT /\ A = {} & not REAL in B ) ; :: thesis: f " (B ` ) = A `
then A6: REAL in ([#] REAL? ) \ B by Th30, XBOOLE_0:def 5;
B ` c= the carrier of REAL? ;
then A7: B ` c= (REAL \ NAT ) \/ {REAL } by Def7;
A8: (B ` ) \ {REAL } c= REAL

proof

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

end;

A10: not REAL in REAL ;
{REAL } c= B `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {REAL } or x in B ` )
assume x in {REAL } ; :: thesis: x in B `
hence x in B ` by A6, TARSKI:def 1; :: thesis: verum

end;

then B ` = ((B ` ) \ {REAL }) \/ {REAL } by XBOOLE_1:45;
then A11: ((id REAL ) +* (NAT --> REAL )) " (B ` ) = ((([#] REAL? ) \ B) \ {REAL }) \/ NAT by A8, A10, Th19
.= ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT by A1, Def7 ;
REAL \ A = ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT

proof

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

proof

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

proof

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

end;

per cases ( x in NAT or not x in NAT ) ;

suppose x in NAT ; :: thesis: x in ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT

hence x in ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in NAT ; :: thesis: x in ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT

then x in REAL \ NAT by A12, XBOOLE_0:def 5;
then x in (REAL \ NAT ) \/ {REAL } by XBOOLE_0:def 3;
then x in ((REAL \ NAT ) \/ {REAL }) \ A by A13, XBOOLE_0:def 5;
then x in (((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL } by A14, XBOOLE_0:def 5;
hence x in ((((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL }) \/ NAT by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

per cases ( x in NAT or x in (((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL } ) by A15, XBOOLE_0:def 3;

suppose A16: x in NAT ; :: thesis: x in REAL \ A

then not x in A by A5, XBOOLE_0:def 4;
hence x in REAL \ A by A16, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A17: x in (((REAL \ NAT ) \/ {REAL }) \ A) \ {REAL } ; :: thesis: x in REAL \ A

then ( x in ((REAL \ NAT ) \/ {REAL }) \ A & not x in {REAL } ) by XBOOLE_0:def 5;
then A18: ( x in (REAL \ NAT ) \/ {REAL } & not x in A ) by XBOOLE_0:def 5;
( x in REAL \ NAT or x in {REAL } ) by A17, XBOOLE_0:def 3;
hence x in REAL \ A by A17, A18, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence f " (B ` ) = A ` by A2, A11, TOPMETR:24; :: thesis: verum

end;

thus ( NAT /\ A = {} & A is open implies ( not REAL in B & B is open ) ) :: thesis: ( not REAL in B & B is open implies ( NAT /\ A = {} & A is open ) )

proof

assume A19: ( NAT /\ A = {} & A is open ) ; :: thesis: ( not REAL in B & B is open )
hence not REAL in B by A1, Th32; :: thesis: B is open
A ` is closed by A19, TOPS_1:30;
then B ` is closed by A1, A3, A4, A19, Th32;
hence B is open by TOPS_1:30; :: thesis: verum

end;

assume A20: ( not REAL in B & B is open ) ; :: thesis: ( NAT /\ A = {} & A is open )
hence NAT /\ A = {} by A1, Th32; :: thesis: A is open
B ` is closed by A20, TOPS_1:30;
then A ` is closed by A1, A3, A4, A20, Th32;
hence A is open by TOPS_1:30; :: thesis: verum