reconsider c = 1 as Element of {0,1,2} by ENUMSET1:def 1;
take c ; :: thesis: c = 1
thus c = 1 ; :: thesis: verum