let a be Nat; :: thesis: for t being Integer holds
( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )
let t be Integer; :: thesis: ( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )
assume |.t.| < a ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )
then A2: ( t < a & t > - a ) by SEQ_2:1;

per cases ( t >= 0 or t < 0 ) ;

suppose B1: t >= 0 ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )

then t mod a = t by A2, NAT_D:63;
hence ( t mod a = |.t.| or t mod a = a - |.t.| ) by B1, ABSVALUE:def 1; :: thesis: verum

end;

suppose B1: t < 0 ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )

then t mod a = a + t by A2, NAT_D:63
.= a - (- t)
.= a - |.t.| by B1, ABSVALUE:def 1 ;
hence ( t mod a = |.t.| or t mod a = a - |.t.| ) ; :: thesis: verum

end;

end;