let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0,1} or x in REAL )
assume x in {0,1} ; :: thesis: x in REAL
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence x in REAL by NUMBERS:19; :: thesis: verum