let x be set ; :: 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 Def7; :: thesis: verum