let i, j be Nat; :: thesis: ( 0 < i implies j mod i < i )
assume 0 < i ; :: thesis: j mod i < i
then ex t being Nat st
( j = (i * t) + (j mod i) & j mod i < i ) by Def2;
hence j mod i < i ; :: thesis: verum