let x be object ; :: according to MEMBERED:def 2 :: thesis: ( not x in ].r,s.[ or x is ext-real )
assume x in ].r,s.[ ; :: thesis: x is ext-real
then ex a being Element of ExtREAL st
( x = a & r < a & a < s ) ;
hence x is ext-real ; :: thesis: verum