theorem :: NUMBER03:55

for a, b, c being Prime st a,b,c are_mutually_distinct holds
a,b,c are_mutually_coprime by INT_2:30;