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