for X1, X2, X3, X4 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 A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )