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

consider f being Function of R^1,REAL? such that
A1: f = () +* () 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) \/ ) ) :: thesis: ( ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ ) 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) \/ )

consider O being Subset of R^1 such that
A5: O = (f " (A `)) ` ;
A ` is closed by ;
then f " (A `) is closed by A2;
then A6: (f " (A `)) ` is open by TOPS_1:3;
A7: not REAL in () \ A by ;
A8: A ` c= (A `) \
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ` or x in (A `) \ )
assume A9: x in A ` ; :: thesis: x in (A `) \
then not x in by ;
hence x in (A `) \ by ; :: thesis: verum
end;
A ` c= the carrier of REAL? ;
then A10: A ` c= () \/ by Def8;
A11: A ` c= REAL \ NAT
proof
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:
then ( x in REAL \ NAT or x in ) by ;
hence x in REAL \ NAT by ; :: thesis: verum
end;
(A `) \ c= A ` by XBOOLE_1:36;
then A13: A ` = (A `) \ by A8;
not REAL in REAL ;
then ((id REAL) +* ()) " ((A `) \ ) = (A `) \ NAT by ;
then O = (() \ (A `)) \/ (NAT /\ ()) by ;
then A14: O = (() \ (A `)) \/ NAT by ;
A = (A `) `
.= the carrier of REAL? \ (A `) ;
then A15: A = (() \/ ) \ (A `) by Def8;
A16: A = ((REAL \ (A `)) \ NAT) \/
proof
thus A c= ((REAL \ (A `)) \ NAT) \/ :: according to XBOOLE_0:def 10 :: thesis: ((REAL \ (A `)) \ NAT) \/ c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in ((REAL \ (A `)) \ NAT) \/ )
assume A17: x in A ; :: thesis: x in ((REAL \ (A `)) \ NAT) \/
then A18: not x in A ` by XBOOLE_0:def 5;
( x in REAL \ NAT or x in ) by ;
then ( ( x in REAL \ (A `) & not x in NAT ) or x in ) by ;
then ( x in (REAL \ (A `)) \ NAT or x in ) by XBOOLE_0:def 5;
hence x in ((REAL \ (A `)) \ NAT) \/ by XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((REAL \ (A `)) \ NAT) \/ or x in A )
assume x in ((REAL \ (A `)) \ NAT) \/ ; :: thesis: x in A
then ( x in (REAL \ (A `)) \ NAT or x in ) by XBOOLE_0:def 3;
then A19: ( ( x in REAL \ (A `) & not x in NAT ) or ( x in & not x in A ` ) ) by ;
then ( x in REAL \ NAT or x in ) by XBOOLE_0:def 5;
then A20: x in () \/ by XBOOLE_0:def 3;
not x in A ` by ;
hence x in A by ; :: thesis: verum
end;
NAT c= REAL \ (A `)
proof
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 ;
hence x in REAL \ (A `) by ; :: thesis: verum
end;
then O = REAL \ (A `) by ;
hence ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ ) by ; :: 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) \/ ; :: thesis: ( A is open & REAL in A )
consider B being Subset of R^1 such that
A25: B = () \ O ;
not REAL in REAL ;
then ((id REAL) +* ()) " (() \ ) = () \ NAT by Th19;
then A26: f " (() \ ) = REAL \ () by ;
A27: B is closed by ;
A ` = (() \/ ) \ ((O \ NAT) \/ ) by
.= (() \ ((O \ NAT) \/ )) \/ ( \ ( \/ (O \ NAT))) by XBOOLE_1:42
.= (() \ ((O \ NAT) \/ )) \/ {} by XBOOLE_1:46
.= (() \ (O \ NAT)) \ by XBOOLE_1:41
.= (REAL \ (NAT \/ (O \ NAT))) \ by XBOOLE_1:41
.= (REAL \ ()) \ by XBOOLE_1:39
.= () \ by ;
then f " (A `) = B by ;
then ([#] REAL?) \ A is closed by ;
hence A is open by Lm2; :: thesis:
REAL in by TARSKI:def 1;
hence REAL in A by ; :: thesis: verum