let e be set ; :: according to MEMBERED:def 2 :: thesis: ( not e in {a,b,c,d} or e is ext-real )
thus ( not e in {a,b,c,d} or e is ext-real ) by ENUMSET1:def 2; :: thesis: verum