let X1, X2, X3, X4 be non empty set ; :: thesis: 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 )
let A1 be non empty Subset of X1; :: thesis: 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 )
let A2 be non empty Subset of X2; :: thesis: 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 )
let A3 be non empty Subset of X3; :: thesis: 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 )
let A4 be non empty Subset of X4; :: thesis: 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 )
let x be Element of [:X1,X2,X3,X4:]; :: thesis: ( x in [:A1,A2,A3,A4:] implies ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 ) )
assume x in [:A1,A2,A3,A4:] ; :: thesis: ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
then reconsider y = x as Element of [:A1,A2,A3,A4:] ;
A1: y `2_4 in A2 ;
A2: y `4_4 in A4 ;
A3: y `3_4 in A3 ;
y `1_4 in A1 ;
hence ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 ) by A1, A3, A2; :: thesis: verum