for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )