:: deftheorem defines are_mutually_disjoint PREFER_1:def 1 :
for X, Y, Z being set holds
( X,Y,Z are_mutually_disjoint iff ( X misses Y & Y misses Z & X misses Z ) );