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 that
A1: A is Subset of REAL? and
A2: not REAL in A ; :: thesis: ( A is Subset of R^1 & NAT /\ A = {} )
A c= the carrier of REAL? by A1;
then A3: A c= (REAL \ NAT) \/ {REAL} by Def8;
A c= REAL

proof

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

end;

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

proof

set x = the Element of NAT /\ A;
assume A5: NAT /\ A <> {} ; :: thesis: contradiction
then A6: the Element of NAT /\ A in NAT by XBOOLE_0:def 4;
A7: the Element of NAT /\ A in A by A5, XBOOLE_0:def 4;

per cases ( the Element of NAT /\ A in REAL \ NAT or the Element of NAT /\ A in {REAL} ) by A3, A7, XBOOLE_0:def 3;

suppose the Element of NAT /\ A in REAL \ NAT ; :: thesis: contradiction

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

end;

suppose the Element of NAT /\ A in {REAL} ; :: thesis: contradiction

then the Element of NAT /\ A = REAL by TARSKI:def 1;
then REAL in REAL by A6, NUMBERS:19;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

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

end;

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

proof

assume REAL in A ; :: thesis: contradiction
then REAL in REAL by A8, TOPMETR:17;
hence contradiction ; :: thesis: verum

end;