let x be Variable; not x in {0,1,2,3,4}
assume
x in {0,1,2,3,4}
; contradiction
then
x in {0,1} \/ {2,3,4}
by ENUMSET1:8;
then
( x in {0,1} or x in {2,3,4} )
by XBOOLE_0:def 3;
then A1:
( x = 0 or x = 1 or x = 2 or x = 3 or x = 4 )
by ENUMSET1:def 1, TARSKI:def 2;
x in VAR
;
then
ex i being Element of NAT st
( x = i & 5 <= i )
;
hence
contradiction
by A1; verum