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 = () +* () 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 = (((() \/ ) \ A) \ ) \/ NAT
proof
thus REAL \ A c= (((() \/ ) \ A) \ ) \/ NAT :: according to XBOOLE_0:def 10 :: thesis: (((() \/ ) \ A) \ ) \/ NAT c= REAL \ A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL \ A or x in (((() \/ ) \ A) \ ) \/ NAT )
assume A8: x in REAL \ A ; :: thesis: x in (((() \/ ) \ A) \ ) \/ NAT
then A9: not x in A by XBOOLE_0:def 5;
A10: x in REAL by A8;
A11: not x in
proof
assume x in ; :: 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;
per cases ( x in NAT or not x in NAT ) ;
suppose x in NAT ; :: thesis: x in (((() \/ ) \ A) \ ) \/ NAT
hence x in (((() \/ ) \ A) \ ) \/ NAT by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not x in NAT ; :: thesis: x in (((() \/ ) \ A) \ ) \/ NAT
then x in REAL \ NAT by ;
then x in () \/ by XBOOLE_0:def 3;
then x in (() \/ ) \ A by ;
then x in ((() \/ ) \ A) \ by ;
hence x in (((() \/ ) \ A) \ ) \/ NAT by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (((() \/ ) \ A) \ ) \/ NAT or x in REAL \ A )
assume A12: x in (((() \/ ) \ A) \ ) \/ NAT ; :: thesis: x in REAL \ A
end;
B ` c= the carrier of REAL? ;
then A16: B ` c= () \/ by Def8;
A17: (B `) \ c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B `) \ or x in REAL )
assume A18: x in (B `) \ ; :: thesis:
then x in B ` by XBOOLE_0:def 5;
then ( x in REAL \ NAT or x in ) by ;
hence x in REAL by ; :: thesis: verum
end;
A19: REAL in () \ B by ;
{REAL} c= B ` by ;
then ( not REAL in REAL & B ` = ((B `) \ ) \/ ) by XBOOLE_1:45;
then (() +* ()) " (B `) = ((() \ B) \ ) \/ NAT by
.= (((() \/ ) \ A) \ ) \/ NAT by ;
hence f " (B `) = A ` by ; :: 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 ; :: thesis: B is open
A ` is closed by ;
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 ; :: thesis: A is open
B ` is closed by ;
then A ` is closed by A3, A2, A4, A22, Th29;
hence A is open by TOPS_1:4; :: thesis: verum