let e be set ; :: according to MEMBERED:def 5 :: thesis: ( e in {i1,i2,i3} implies e is integer )
thus ( e in {i1,i2,i3} implies e is integer ) by ENUMSET1:def 1; :: thesis: verum