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