:: deftheorem defines are_mutually_coprime NUMBER03:def 1 :
for a, b, c being Integer holds
( a,b,c are_mutually_coprime iff ( a,b are_coprime & a,c are_coprime & b,c are_coprime ) );