let m be non zero Nat; :: thesis: for x being Integer holds x mod m in Segm m
let x be Integer; :: thesis: x mod m in Segm m
( x mod m >= 0 & x mod m < m ) by NAT_D:62;
then x mod m in NAT by INT_1:3;
hence x mod m in Segm m by NAT_1:44, NAT_D:62; :: thesis: verum