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 ) )
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: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
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;
A ` c= the carrier of REAL? ;
then A10: A ` c= (REAL \ NAT) \/ {REAL} 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: 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;
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
thus A c= ((REAL \ (A `)) \ NAT) \/ {REAL} :: according to XBOOLE_0:def 10 :: thesis: ((REAL \ (A `)) \ NAT) \/ {REAL} c= A
proof
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;
let x be object ; :: 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 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;
then O = REAL \ (A `) by A14, TOPMETR:17, 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 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