let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ].a,b.] where a, b is Real : a <= b } or x in bool REAL )
assume x in { ].a,b.] where a, b is Real : a <= b } ; :: thesis: x in bool REAL
then ex a0, b0 being Real st
( x = ].a0,b0.] & a0 <= b0 ) ;
hence x in bool REAL ; :: thesis: verum