let x be object ; :: according to MEMBERED:def 2 :: thesis: ( x in ExtREAL implies x is ext-real )
thus ( x in ExtREAL implies x is ext-real ) ; :: thesis: verum