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