let a be Nat; :: thesis: for b being non zero Nat st a > b holds
ex p being prime Nat st p |-count a > p |-count b
let b be non zero Nat; :: thesis: ( a > b implies ex p being prime Nat st p |-count a > p |-count b )
assume A1: a > b ; :: thesis: ex p being prime Nat st p |-count a > p |-count b
then reconsider a = a as non zero Nat ;
( ( for p being prime Nat holds p |-count a <= p |-count b ) implies a <= b )
proof
assume for p being prime Nat holds p |-count a <= p |-count b ; :: thesis: a <= b
then for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ;
then consider c being Element of NAT such that
B1: b = a * c by NAT_4:20;
not c is zero by B1;
then a * c >= a * 1 by NAT_1:14, XREAL_1:64;
hence a <= b by B1; :: thesis: verum
end;
hence ex p being prime Nat st p |-count a > p |-count b by A1; :: thesis: verum