let a be non trivial Nat; :: thesis: for p being prime Nat st p > a holds
( not p divides a & not a divides p )
let p be prime Nat; :: thesis: ( p > a implies ( not p divides a & not a divides p ) )
assume p > a ; :: thesis: ( not p divides a & not a divides p )
then a,p are_coprime by NAT_6:6, NAT_D:7;
hence ( not p divides a & not a divides p ) by NTC; :: thesis: verum