let x be object ; :: according to VALUED_2:def 4 :: thesis: ( not x in REAL n or x is set )
assume x in REAL n ; :: thesis: x is set
then reconsider x = x as Element of REAL n ;
x is real-valued ;
hence x is set ; :: thesis: verum