let i be Integer; :: thesis: ( not |.i.| <= 2 or i = - 2 or i = - 1 or i = 0 or i = 1 or i = 2 )
assume |.i.| <= 2 ; :: thesis: ( i = - 2 or i = - 1 or i = 0 or i = 1 or i = 2 )
then not not |.i.| = 0 & ... & not |.i.| = 2 ;
hence ( i = - 2 or i = - 1 or i = 0 or i = 1 or i = 2 ) by ABSVALUE:2, Th2; :: thesis: verum