consider m being Integer, k being Nat such that
A1:
k <> 0
and
A2:
p = m / k
and
A3:
for n being Integer
for w being Nat st w <> 0 & p = n / w holds
k <= w
by Th6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take IT = k; ( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
IT <= k ) )
thus
( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
IT <= k ) )
by A1, A2, A3; verum