:: deftheorem defines are_mutually_distinct ZFMISC_1:def 5 :
for x1, x2, x3 being object holds
( x1,x2,x3 are_mutually_distinct iff ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) );