let h, s be non zero Nat; :: thesis: ( ( for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ) implies support (prime_factorization s) c= support (prime_factorization h) )

assume A1: for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ; :: thesis: support (prime_factorization s) c= support (prime_factorization h)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (prime_factorization s) or x in support (prime_factorization h) )

assume A2: x in support (prime_factorization s) ; :: thesis: x in support (prime_factorization h)

then reconsider q = x as Prime by NEWTON:def 6;

q divides h by Th5, A2, A1;

then q in support (pfexp h) by ORDINAL1:def 13, NAT_3:37;

hence x in support (prime_factorization h) by NAT_3:def 9; :: thesis: verum

not q,h are_coprime ) implies support (prime_factorization s) c= support (prime_factorization h) )

assume A1: for q being Prime st q in support (prime_factorization s) holds

not q,h are_coprime ; :: thesis: support (prime_factorization s) c= support (prime_factorization h)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (prime_factorization s) or x in support (prime_factorization h) )

assume A2: x in support (prime_factorization s) ; :: thesis: x in support (prime_factorization h)

then reconsider q = x as Prime by NEWTON:def 6;

q divides h by Th5, A2, A1;

then q in support (pfexp h) by ORDINAL1:def 13, NAT_3:37;

hence x in support (prime_factorization h) by NAT_3:def 9; :: thesis: verum