let e be set ; :: according to MEMBERED:def 2 :: thesis: ( e in {e1,e2,e3} implies e is ext-real )
thus ( e in {e1,e2,e3} implies e is ext-real ) by ENUMSET1:def 1; :: thesis: verum