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