for X1, X2, X3 being non empty set
for A1 being non empty Subset of X1
for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )