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