let k, l be Nat; :: thesis: ( k <> 0 & ex m being Integer st p = m / k & ( for n being Integer

for k being Nat st k <> 0 & p = n / k holds

k <= k ) & l <> 0 & ex m being Integer st p = m / l & ( for n being Integer

for k being Nat st k <> 0 & p = n / k holds

l <= k ) implies k = l )

assume that

A4: k <> 0 and

A5: ex m being Integer st p = m / k and

A6: for m1 being Integer

for k1 being Nat st k1 <> 0 & p = m1 / k1 holds

k <= k1 and

A7: l <> 0 and

A8: ex n being Integer st p = n / l and

A9: for n1 being Integer

for k1 being Nat st k1 <> 0 & p = n1 / k1 holds

l <= k1 ; :: thesis: k = l

A10: l <= k by A4, A5, A9;

k <= l by A6, A7, A8;

hence k = l by A10, XXREAL_0:1; :: thesis: verum

for k being Nat st k <> 0 & p = n / k holds

k <= k ) & l <> 0 & ex m being Integer st p = m / l & ( for n being Integer

for k being Nat st k <> 0 & p = n / k holds

l <= k ) implies k = l )

assume that

A4: k <> 0 and

A5: ex m being Integer st p = m / k and

A6: for m1 being Integer

for k1 being Nat st k1 <> 0 & p = m1 / k1 holds

k <= k1 and

A7: l <> 0 and

A8: ex n being Integer st p = n / l and

A9: for n1 being Integer

for k1 being Nat st k1 <> 0 & p = n1 / k1 holds

l <= k1 ; :: thesis: k = l

A10: l <= k by A4, A5, A9;

k <= l by A6, A7, A8;

hence k = l by A10, XXREAL_0:1; :: thesis: verum