let e be set ; :: according to MEMBERED:def 6 :: thesis: ( e in {n1,n2,n3} implies e is natural )
thus ( e in {n1,n2,n3} implies e is natural ) by ENUMSET1:def 1; :: thesis: verum