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