let a be Nat; :: thesis: for b, c being non zero Nat holds (a mod c) * (b mod c) >= (a * b) mod c
let b, c be non zero Nat; :: thesis: (a mod c) * (b mod c) >= (a * b) mod c
((a mod c) * (b mod c)) mod c <= (a mod c) * (b mod c) by AMB;
hence (a mod c) * (b mod c) >= (a * b) mod c by NAT_D:67; :: thesis: verum