let m, n be Nat; :: thesis: ( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m )
( m <= n or n <= m ) ;
hence ( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m ) by NEWTON:69; :: thesis: verum