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