let x be set ; :: according to MEMBERED:def 3,TOPMETR:def 8 :: thesis: ( not x in the carrier of R^1 or x is real )
assume x in the carrier of R^1 ; :: thesis: x is real
hence x is real ; :: thesis: verum