let X1, X2, X3, X4 be set ; :: thesis: for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
let A1 be Subset of X1; :: thesis: for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
let A2 be Subset of X2; :: thesis: for A3 being Subset of X3
for A4 being Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
let A3 be Subset of X3; :: thesis: for A4 being Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
let A4 be Subset of X4; :: thesis: for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
let x be Element of [:X1,X2,X3,X4:]; :: thesis: ( x in [:A1,A2,A3,A4:] implies ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 ) )
assume A1: x in [:A1,A2,A3,A4:] ; :: thesis: ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
then A2: ( A1 <> {} & A2 <> {} & A3 <> {} & A4 <> {} ) by Th55;
reconsider y = x as Element of [:A1,A2,A3,A4:] by A1;
( y `1 in A1 & y `2 in A2 & y `3 in A3 & y `4 in A4 ) by A2;
hence ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 ) by Th86; :: thesis: verum