let e be set ; :: according to MEMBERED:def 1 :: thesis: ( e in {c1,c2,c3} implies e is complex )
thus ( e in {c1,c2,c3} implies e is complex ) by ENUMSET1:def 1; :: thesis: verum