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= () \/ 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:
then ( x in REAL \ NAT or x in ) by ;
hence x in REAL by ; :: thesis: verum
end;
hence A is Subset of R^1 by TOPMETR:17; :: thesis:
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 ;
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:
then not x in NAT by ;
hence x in REAL \ NAT by ; :: thesis: verum
end;
REAL \ NAT c= () \/ by XBOOLE_1:7;
then A c= () \/ 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 ;
hence contradiction ; :: thesis: verum
end;