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 ) ) )

consider f being Function of R^1,REAL? such that

A1: f = (id REAL) +* (NAT --> REAL) and

A2: for A being Subset of REAL? holds

( A is closed iff f " A is closed ) by Def8;

assume A3: A = B ; :: thesis: ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )

A4: ( NAT /\ A = {} & not REAL in B implies f " (B `) = A ` )

A22: not REAL in B and

A23: B is open ; :: thesis: ( NAT /\ A = {} & A is open )

thus NAT /\ A = {} by A3, A22, Th29; :: thesis: A is open

B ` is closed by A23, TOPS_1:4;

then A ` is closed by A3, A2, A4, A22, Th29;

hence A is open by TOPS_1:4; :: thesis: verum

( 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 ) ) )

consider f being Function of R^1,REAL? such that

A1: f = (id REAL) +* (NAT --> REAL) and

A2: for A being Subset of REAL? holds

( A is closed iff f " A is closed ) by Def8;

assume A3: A = B ; :: thesis: ( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )

A4: ( NAT /\ A = {} & not REAL in B implies f " (B `) = A ` )

proof

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 ) )
assume that

A5: NAT /\ A = {} and

A6: not REAL in B ; :: thesis: f " (B `) = A `

A7: REAL \ A = ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT

then A16: B ` c= (REAL \ NAT) \/ {REAL} by Def8;

A17: (B `) \ {REAL} c= REAL

{REAL} c= B ` by A19, TARSKI:def 1;

then ( not REAL in REAL & B ` = ((B `) \ {REAL}) \/ {REAL} ) by XBOOLE_1:45;

then ((id REAL) +* (NAT --> REAL)) " (B `) = ((([#] REAL?) \ B) \ {REAL}) \/ NAT by A17, Th18

.= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by A3, Def8 ;

hence f " (B `) = A ` by A1, A7, TOPMETR:17; :: thesis: verum

end;A5: NAT /\ A = {} and

A6: not REAL in B ; :: thesis: f " (B `) = A `

A7: REAL \ A = ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT

proof

B ` c= the carrier of REAL?
;
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

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

end;proof

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

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

then A9: not x in A by XBOOLE_0:def 5;

A10: x in REAL by A8;

A11: not x in {REAL}

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

then A9: not x in A by XBOOLE_0:def 5;

A10: x in REAL by A8;

A11: 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, A10; :: 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, A10; :: thesis: verum

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

end;

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

then
x in REAL \ NAT
by A8, XBOOLE_0:def 5;

then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def 3;

then x in ((REAL \ NAT) \/ {REAL}) \ A by A9, XBOOLE_0:def 5;

then x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} by A11, XBOOLE_0:def 5;

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

end;then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def 3;

then x in ((REAL \ NAT) \/ {REAL}) \ A by A9, XBOOLE_0:def 5;

then x in (((REAL \ NAT) \/ {REAL}) \ A) \ {REAL} by A11, XBOOLE_0:def 5;

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

assume A12: 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 A12, XBOOLE_0:def 3;

end;

suppose A13:
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 A13, XBOOLE_0:def 5, NUMBERS:19; :: thesis: verum

end;hence x in REAL \ A by A13, XBOOLE_0:def 5, NUMBERS:19; :: thesis: verum

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

then
x in ((REAL \ NAT) \/ {REAL}) \ A
by XBOOLE_0:def 5;

then A15: not x in A by XBOOLE_0:def 5;

( x in REAL \ NAT or x in {REAL} ) by A14, XBOOLE_0:def 3;

hence x in REAL \ A by A14, A15, XBOOLE_0:def 5; :: thesis: verum

end;then A15: not x in A by XBOOLE_0:def 5;

( x in REAL \ NAT or x in {REAL} ) by A14, XBOOLE_0:def 3;

hence x in REAL \ A by A14, A15, XBOOLE_0:def 5; :: thesis: verum

then A16: B ` c= (REAL \ NAT) \/ {REAL} by Def8;

A17: (B `) \ {REAL} c= REAL

proof

A19:
REAL in ([#] REAL?) \ B
by A6, Th27, XBOOLE_0:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B `) \ {REAL} or x in REAL )

assume A18: x in (B `) \ {REAL} ; :: thesis: x in REAL

then x in B ` by XBOOLE_0:def 5;

then ( x in REAL \ NAT or x in {REAL} ) by A16, XBOOLE_0:def 3;

hence x in REAL by A18, XBOOLE_0:def 5; :: thesis: verum

end;assume A18: x in (B `) \ {REAL} ; :: thesis: x in REAL

then x in B ` by XBOOLE_0:def 5;

then ( x in REAL \ NAT or x in {REAL} ) by A16, XBOOLE_0:def 3;

hence x in REAL by A18, XBOOLE_0:def 5; :: thesis: verum

{REAL} c= B ` by A19, TARSKI:def 1;

then ( not REAL in REAL & B ` = ((B `) \ {REAL}) \/ {REAL} ) by XBOOLE_1:45;

then ((id REAL) +* (NAT --> REAL)) " (B `) = ((([#] REAL?) \ B) \ {REAL}) \/ NAT by A17, Th18

.= ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT by A3, Def8 ;

hence f " (B `) = A ` by A1, A7, TOPMETR:17; :: thesis: verum

proof

assume that
assume that

A20: NAT /\ A = {} and

A21: A is open ; :: thesis: ( not REAL in B & B is open )

thus not REAL in B by A3, A20, Th29; :: thesis: B is open

A ` is closed by A21, TOPS_1:4;

then B ` is closed by A3, A2, A4, A20, Th29;

hence B is open by TOPS_1:4; :: thesis: verum

end;A20: NAT /\ A = {} and

A21: A is open ; :: thesis: ( not REAL in B & B is open )

thus not REAL in B by A3, A20, Th29; :: thesis: B is open

A ` is closed by A21, TOPS_1:4;

then B ` is closed by A3, A2, A4, A20, Th29;

hence B is open by TOPS_1:4; :: thesis: verum

A22: not REAL in B and

A23: B is open ; :: thesis: ( NAT /\ A = {} & A is open )

thus NAT /\ A = {} by A3, A22, Th29; :: thesis: A is open

B ` is closed by A23, TOPS_1:4;

then A ` is closed by A3, A2, A4, A22, Th29;

hence A is open by TOPS_1:4; :: thesis: verum