let a, b be Nat; :: thesis: PrimeDivisors (a * b) = (PrimeDivisors a) \/ (PrimeDivisors b)
thus PrimeDivisors (a * b) c= (PrimeDivisors a) \/ (PrimeDivisors b) :: according to XBOOLE_0:def 10 :: thesis: (PrimeDivisors a) \/ (PrimeDivisors b) c= PrimeDivisors (a * b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors (a * b) or x in (PrimeDivisors a) \/ (PrimeDivisors b) )
assume x in PrimeDivisors (a * b) ; :: thesis: x in (PrimeDivisors a) \/ (PrimeDivisors b)
then consider k being Prime such that
A1: ( x = k & k divides a * b ) ;
( k divides a or k divides b ) by A1, NAT_6:7;
then ( x in PrimeDivisors a or x in PrimeDivisors b ) by A1;
hence x in (PrimeDivisors a) \/ (PrimeDivisors b) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (PrimeDivisors a) \/ (PrimeDivisors b) or x in PrimeDivisors (a * b) )
assume x in (PrimeDivisors a) \/ (PrimeDivisors b) ; :: thesis: x in PrimeDivisors (a * b)

per cases then ( x in PrimeDivisors a or x in PrimeDivisors b ) by XBOOLE_0:def 3;

suppose x in PrimeDivisors a ; :: thesis: x in PrimeDivisors (a * b)

then consider k being Prime such that
A1: ( x = k & k divides a ) ;
k divides a * b by A1, INT_2:2;
hence x in PrimeDivisors (a * b) by A1; :: thesis: verum

end;

suppose x in PrimeDivisors b ; :: thesis: x in PrimeDivisors (a * b)

then consider k being Prime such that
A1: ( x = k & k divides b ) ;
k divides a * b by A1, INT_2:2;
hence x in PrimeDivisors (a * b) by A1; :: thesis: verum

end;

end;