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 ` )
proof
assume that
A5: NAT /\ A = {} and
A6: not REAL in B ; :: thesis: f " (B `) = A `
A7: REAL \ A = ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT
proof
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
proof
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}
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;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT or x in REAL \ A )
assume A12: x in ((((REAL \ NAT) \/ {REAL}) \ A) \ {REAL}) \/ NAT ; :: thesis: x in REAL \ A
end;
B ` c= the carrier of REAL? ;
then A16: B ` c= (REAL \ NAT) \/ {REAL} by Def8;
A17: (B `) \ {REAL} c= REAL
proof
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;
A19: REAL in ([#] REAL?) \ B by A6, Th27, XBOOLE_0:def 5;
{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;
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 ) )
proof
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;
assume that
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