let S be Subset of ExtREAL ; :: thesis: S is ext-real-membered
let x be set ; :: according to MEMBERED:def 2 :: thesis: ( x in S implies x is ext-real )
thus ( x in S implies x is ext-real ) by XXREAL_0:def 1; :: thesis: verum