let e be set ; :: according to MEMBERED:def 3 :: thesis: ( e in {r1,r2,r3} implies e is real )
thus ( e in {r1,r2,r3} implies e is real ) by ENUMSET1:def 1; :: thesis: verum