let x be Variable; :: thesis: ( x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )
x in VAR ;
then A1: ex i being Element of NAT st
( x = i & 5 <= i ) ;
assume ( x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum