let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {REAL} or x in the carrier of REAL? )
assume x in {REAL} ; :: thesis: x in the carrier of REAL?
then x in (REAL \ NAT) \/ {REAL} by XBOOLE_0:def 3;
hence x in the carrier of REAL? by Def8; :: thesis: verum