set X = {'not','&','='};
{'not','&','='} is FinSequence-membered by ENUMSET1:def 1;
hence {'not','&','='} is non empty FinSequence-membered set by ENUMSET1:def 1; :: thesis: verum