let m, n be non zero Nat; :: thesis: ( ( for p being Prime holds p |-count m <= p |-count n ) implies support (ppf m) c= support (ppf n) )
assume A1: for p being Prime holds p |-count m <= p |-count n ; :: thesis: support (ppf m) c= support (ppf n)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf m) or x in support (ppf n) )
assume A2: x in support (ppf m) ; :: thesis: x in support (ppf n)
then x in support (pfexp m) by NAT_3:def 9;
then reconsider p = x as Prime by NAT_3:34;
(ppf m) . p <> 0 by A2, PRE_POLY:def 7;
then p |-count m <> 0 by NAT_3:55;
then p |-count n > 0 by A1;
then (ppf n) . p = p |^ (p |-count n) by NAT_3:56;
hence x in support (ppf n) by PRE_POLY:def 7; :: thesis: verum