let A be set ; :: thesis: ( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) )
thus ( A is Subset of REAL? & not REAL in A implies ( A is Subset of R^1 & NAT /\ A = {} ) ) :: thesis: ( A is Subset of R^1 & NAT /\ A = {} implies ( A is Subset of REAL? & not REAL in A ) )

proof

assume A1: ( A is Subset of REAL? & not REAL in A ) ; :: thesis: ( A is Subset of R^1 & NAT /\ A = {} )
then A c= the carrier of REAL? ;
then A2: A c= (REAL \ NAT ) \/ {REAL } by Def7;
A c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in REAL )
assume A3: x in A ; :: thesis: x in REAL
then ( x in REAL \ NAT or x in {REAL } ) by A2, XBOOLE_0:def 3;
hence x in REAL by A1, A3, TARSKI:def 1; :: thesis: verum

end;

hence A is Subset of R^1 by TOPMETR:24; :: thesis: NAT /\ A = {}
thus NAT /\ A = {} :: thesis: verum

proof

assume A4: NAT /\ A <> {} ; :: thesis: contradiction
consider x being Element of NAT /\ A;
A5: ( x in NAT & x in A ) by A4, XBOOLE_0:def 4;

per cases ( x in REAL \ NAT or x in {REAL } ) by A2, A5, XBOOLE_0:def 3;

suppose x in REAL \ NAT ; :: thesis: contradiction

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

suppose x in {REAL } ; :: thesis: contradiction

then x = REAL by TARSKI:def 1;
then REAL in REAL by A5;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

assume A6: ( A is Subset of R^1 & NAT /\ A = {} ) ; :: thesis: ( A is Subset of REAL? & not REAL in A )
A7: 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 A8: x in A ; :: thesis: x in REAL \ NAT
then not x in NAT by A6, XBOOLE_0:def 4;
hence x in REAL \ NAT by A6, A8, TOPMETR:24, XBOOLE_0:def 5; :: thesis: verum

end;

REAL \ NAT c= (REAL \ NAT ) \/ {REAL } by XBOOLE_1:7;
then A c= (REAL \ NAT ) \/ {REAL } by A7, XBOOLE_1:1;
hence A is Subset of REAL? by Def7; :: thesis: not REAL in A
thus not REAL in A :: thesis: verum

proof

assume REAL in A ; :: thesis: contradiction
then REAL in REAL by A6, TOPMETR:24;
hence contradiction ; :: thesis: verum

end;