let j, k be Nat; :: thesis: ( 0 < k & k <= j & k mod j = 0 implies k = j )
assume A1: ( 0 < k & k <= j & k mod j = 0 ) ; :: thesis: k = j
then k >= j by NAT_D:24;
hence k = j by A1, XXREAL_0:1; :: thesis: verum