let p, q be Prime; :: thesis: ( p <> q implies card (PrimeDivisors (p * q)) = 2 )
assume A1: p <> q ; :: thesis: card (PrimeDivisors (p * q)) = 2
PrimeDivisors (p * q) = (PrimeDivisors (p |^ 1)) \/ (PrimeDivisors (q |^ 1)) by NUMBER12:48
.= (PrimeDivisors (p |^ 1)) \/ {q} by NUMBER12:50
.= {p} \/ {q} by NUMBER12:50
.= {p,q} by ENUMSET1:1 ;
hence card (PrimeDivisors (p * q)) = 2 by A1, CARD_2:57; :: thesis: verum