let x be Variable; :: thesis: not x in {0,1,2,3,4}
assume x in {0,1,2,3,4} ; :: thesis: 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; :: thesis: verum