let n, m be Nat; :: thesis: ( n < m iff primenumber n < primenumber m )
AA: for n, m being Nat st n < m holds
primenumber n < primenumber m
proof
let n, m be Nat; :: thesis: ( n < m implies primenumber n < primenumber m )
assume A2: n < m ; :: thesis: primenumber n < primenumber m
assume A3: primenumber n >= primenumber m ; :: thesis: contradiction
n = card (SetPrimenumber (primenumber n)) by NEWTON:def 8;
then A4: card (SetPrimenumber (primenumber n)) < card (SetPrimenumber (primenumber m)) by A2, NEWTON:def 8;
Segm (card (SetPrimenumber (primenumber m))) c= Segm (card (SetPrimenumber (primenumber n))) by CARD_1:11, A3, NEWTON:69;
hence contradiction by A4, NAT_1:39; :: thesis: verum
end;
hence ( n < m implies primenumber n < primenumber m ) ; :: thesis: ( primenumber n < primenumber m implies n < m )
assume A1: primenumber n < primenumber m ; :: thesis: n < m
assume m <= n ; :: thesis: contradiction
then ( m < n or m = n ) by XXREAL_0:1;
hence contradiction by A1, AA; :: thesis: verum