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 Def7;
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

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:30;
then f " (A ` ) is closed by A2;
then A6: (f " (A ` )) ` is open by TOPS_1:29;
A7: not REAL in ([#] REAL? ) \ A by A4, XBOOLE_0:def 5;
A8: A ` c= (A ` ) \ {REAL }

proof

let x be set ; :: 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;

A ` c= the carrier of REAL? ;
then A10: A ` c= (REAL \ NAT ) \/ {REAL } by Def7;
A11: A ` c= REAL \ NAT

proof

let x be set ; :: 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;

(A ` ) \ {REAL } c= A ` by XBOOLE_1:36;
then A13: A ` = (A ` ) \ {REAL } by A8, XBOOLE_0:def 10;
not REAL in REAL ;
then ((id REAL ) +* (NAT --> REAL )) " ((A ` ) \ {REAL }) = (A ` ) \ NAT by A11, Th20, 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:24, XBOOLE_1:28;
A = (A ` ) `
.= the carrier of REAL? \ (A ` ) ;
then A15: A = ((REAL \ NAT ) \/ {REAL }) \ (A ` ) by Def7;
A16: A = ((REAL \ (A ` )) \ NAT ) \/ {REAL }

proof

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

proof

let x be set ; :: 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;

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

NAT c= REAL \ (A ` )

proof

let x be set ; :: 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; :: thesis: verum

end;

then O = REAL \ (A ` ) by A14, TOPMETR:24, XBOOLE_1:12;
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;

given O being Subset of R^1 such that A22: O is open and
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 Th20;
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, Def7
.= ((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:24, 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