let A be Subset of REAL?; :: thesis: ( ( A is open & REAL in A ) iff ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) )

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;

thus ( A is open & REAL in A implies ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) :: thesis: ( ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) implies ( A is open & REAL in A ) )

A23: NAT c= O and

A24: A = (O \ NAT) \/ {REAL} ; :: thesis: ( A is open & REAL in A )

consider B being Subset of R^1 such that

A25: B = ([#] R^1) \ O ;

not REAL in REAL ;

then ((id REAL) +* (NAT --> REAL)) " ((REAL \ O) \ {REAL}) = (REAL \ O) \ NAT by Th19;

then A26: f " ((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1, XBOOLE_1:41;

A27: B is closed by A22, A25, Lm2;

A ` = ((REAL \ NAT) \/ {REAL}) \ ((O \ NAT) \/ {REAL}) by A24, Def8

.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/ (O \ NAT))) by XBOOLE_1:42

.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ {} by XBOOLE_1:46

.= ((REAL \ NAT) \ (O \ NAT)) \ {REAL} by XBOOLE_1:41

.= (REAL \ (NAT \/ (O \ NAT))) \ {REAL} by XBOOLE_1:41

.= (REAL \ (NAT \/ O)) \ {REAL} by XBOOLE_1:39

.= (REAL \ O) \ {REAL} by A23, XBOOLE_1:12 ;

then f " (A `) = B by A23, A25, A26, TOPMETR:17, XBOOLE_1:12;

then ([#] REAL?) \ A is closed by A2, A27;

hence A is open by Lm2; :: thesis: REAL in A

REAL in {REAL} by TARSKI:def 1;

hence REAL in A by A24, XBOOLE_0:def 3; :: thesis: verum

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) )

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;

thus ( A is open & REAL in A implies ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) ) :: thesis: ( ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) implies ( A is open & REAL in A ) )

proof

given O being Subset of R^1 such that A22:
O is open
and
assume that

A3: A is open and

A4: REAL in A ; :: thesis: ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} )

consider O being Subset of R^1 such that

A5: O = (f " (A `)) ` ;

A ` is closed by A3, TOPS_1:4;

then f " (A `) is closed by A2;

then A6: (f " (A `)) ` is open by TOPS_1:3;

A7: not REAL in ([#] REAL?) \ A by A4, XBOOLE_0:def 5;

A8: A ` c= (A `) \ {REAL}

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

A11: A ` c= REAL \ NAT

then A13: A ` = (A `) \ {REAL} by A8;

not REAL in REAL ;

then ((id REAL) +* (NAT --> REAL)) " ((A `) \ {REAL}) = (A `) \ NAT by A11, Th19, XBOOLE_1:1;

then O = (([#] R^1) \ (A `)) \/ (NAT /\ ([#] R^1)) by A1, A5, A13, XBOOLE_1:52;

then A14: O = (([#] R^1) \ (A `)) \/ NAT by TOPMETR:17, XBOOLE_1:28, NUMBERS:19;

A = (A `) `

.= the carrier of REAL? \ (A `) ;

then A15: A = ((REAL \ NAT) \/ {REAL}) \ (A `) by Def8;

A16: A = ((REAL \ (A `)) \ NAT) \/ {REAL}

hence ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) by A5, A6, A14, A16, XBOOLE_1:7; :: thesis: verum

end;A3: A is open and

A4: REAL in A ; :: thesis: ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} )

consider O being Subset of R^1 such that

A5: O = (f " (A `)) ` ;

A ` is closed by A3, TOPS_1:4;

then f " (A `) is closed by A2;

then A6: (f " (A `)) ` is open by TOPS_1:3;

A7: not REAL in ([#] REAL?) \ A by A4, XBOOLE_0:def 5;

A8: A ` c= (A `) \ {REAL}

proof

A ` c= the carrier of REAL?
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ` or x in (A `) \ {REAL} )

assume A9: x in A ` ; :: thesis: x in (A `) \ {REAL}

then not x in {REAL} by A7, TARSKI:def 1;

hence x in (A `) \ {REAL} by A9, XBOOLE_0:def 5; :: thesis: verum

end;assume A9: x in A ` ; :: thesis: x in (A `) \ {REAL}

then not x in {REAL} by A7, TARSKI:def 1;

hence x in (A `) \ {REAL} by A9, XBOOLE_0:def 5; :: thesis: verum

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

A11: A ` c= REAL \ NAT

proof

(A `) \ {REAL} c= A `
by XBOOLE_1:36;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ` or x in REAL \ NAT )

assume A12: x in A ` ; :: thesis: x in REAL \ NAT

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

hence x in REAL \ NAT by A7, A12, TARSKI:def 1; :: thesis: verum

end;assume A12: x in A ` ; :: thesis: x in REAL \ NAT

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

hence x in REAL \ NAT by A7, A12, TARSKI:def 1; :: thesis: verum

then A13: A ` = (A `) \ {REAL} by A8;

not REAL in REAL ;

then ((id REAL) +* (NAT --> REAL)) " ((A `) \ {REAL}) = (A `) \ NAT by A11, Th19, XBOOLE_1:1;

then O = (([#] R^1) \ (A `)) \/ (NAT /\ ([#] R^1)) by A1, A5, A13, XBOOLE_1:52;

then A14: O = (([#] R^1) \ (A `)) \/ NAT by TOPMETR:17, XBOOLE_1:28, NUMBERS:19;

A = (A `) `

.= the carrier of REAL? \ (A `) ;

then A15: A = ((REAL \ NAT) \/ {REAL}) \ (A `) by Def8;

A16: A = ((REAL \ (A `)) \ NAT) \/ {REAL}

proof

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

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

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

then A19: ( ( x in REAL \ (A `) & not x in NAT ) or ( x in {REAL} & not x in A ` ) ) by A7, TARSKI:def 1, XBOOLE_0:def 5;

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

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

not x in A ` by A19, XBOOLE_0:def 5;

hence x in A by A15, A20, XBOOLE_0:def 5; :: thesis: verum

end;proof

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

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

then A18: not x in A ` by XBOOLE_0:def 5;

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

then ( ( x in REAL \ (A `) & not x in NAT ) or x in {REAL} ) by A18, XBOOLE_0:def 5;

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

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

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

then A18: not x in A ` by XBOOLE_0:def 5;

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

then ( ( x in REAL \ (A `) & not x in NAT ) or x in {REAL} ) by A18, XBOOLE_0:def 5;

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

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

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

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

then A19: ( ( x in REAL \ (A `) & not x in NAT ) or ( x in {REAL} & not x in A ` ) ) by A7, TARSKI:def 1, XBOOLE_0:def 5;

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

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

not x in A ` by A19, XBOOLE_0:def 5;

hence x in A by A15, A20, XBOOLE_0:def 5; :: thesis: verum

proof

then
O = REAL \ (A `)
by A14, TOPMETR:17, XBOOLE_1:12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in REAL \ (A `) )

assume A21: x in NAT ; :: thesis: x in REAL \ (A `)

then not x in A ` by A11, XBOOLE_0:def 5;

hence x in REAL \ (A `) by A21, XBOOLE_0:def 5, NUMBERS:19; :: thesis: verum

end;assume A21: x in NAT ; :: thesis: x in REAL \ (A `)

then not x in A ` by A11, XBOOLE_0:def 5;

hence x in REAL \ (A `) by A21, XBOOLE_0:def 5, NUMBERS:19; :: thesis: verum

hence ex O being Subset of R^1 st

( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) by A5, A6, A14, A16, XBOOLE_1:7; :: thesis: verum

A23: NAT c= O and

A24: A = (O \ NAT) \/ {REAL} ; :: thesis: ( A is open & REAL in A )

consider B being Subset of R^1 such that

A25: B = ([#] R^1) \ O ;

not REAL in REAL ;

then ((id REAL) +* (NAT --> REAL)) " ((REAL \ O) \ {REAL}) = (REAL \ O) \ NAT by Th19;

then A26: f " ((REAL \ O) \ {REAL}) = REAL \ (O \/ NAT) by A1, XBOOLE_1:41;

A27: B is closed by A22, A25, Lm2;

A ` = ((REAL \ NAT) \/ {REAL}) \ ((O \ NAT) \/ {REAL}) by A24, Def8

.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ ({REAL} \ ({REAL} \/ (O \ NAT))) by XBOOLE_1:42

.= ((REAL \ NAT) \ ((O \ NAT) \/ {REAL})) \/ {} by XBOOLE_1:46

.= ((REAL \ NAT) \ (O \ NAT)) \ {REAL} by XBOOLE_1:41

.= (REAL \ (NAT \/ (O \ NAT))) \ {REAL} by XBOOLE_1:41

.= (REAL \ (NAT \/ O)) \ {REAL} by XBOOLE_1:39

.= (REAL \ O) \ {REAL} by A23, XBOOLE_1:12 ;

then f " (A `) = B by A23, A25, A26, TOPMETR:17, XBOOLE_1:12;

then ([#] REAL?) \ A is closed by A2, A27;

hence A is open by Lm2; :: thesis: REAL in A

REAL in {REAL} by TARSKI:def 1;

hence REAL in A by A24, XBOOLE_0:def 3; :: thesis: verum