let X1, X2, X3, X4, X5, X6 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 A5 being Subset of X5
for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
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 A5 being Subset of X5
for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let A2 be Subset of X2; :: thesis: for A3 being Subset of X3
for A4 being Subset of X4
for A5 being Subset of X5
for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let A3 be Subset of X3; :: thesis: for A4 being Subset of X4
for A5 being Subset of X5
for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let A4 be Subset of X4; :: thesis: for A5 being Subset of X5
for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let A5 be Subset of X5; :: thesis: for A6 being Subset of X6
for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let A6 be Subset of X6; :: thesis: for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
let x be Element of [:X1,X2,X3,X4,X5,X6:]; :: thesis: ( x in [:A1,A2,A3,A4,A5,A6:] implies ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 ) )
assume A1: x in [:A1,A2,A3,A4,A5,A6:] ; :: thesis: ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )
then reconsider y = x as Element of [:A1,A2,A3,A4,A5,A6:] ;
A2 <> {} by A1, Th51;
then A2: y `2 in A2 ;
A6 <> {} by A1, Th51;
then A3: y `6 in A6 ;
A5 <> {} by A1, Th51;
then A4: y `5 in A5 ;
A4 <> {} by A1, Th51;
then A5: y `4 in A4 ;
A3 <> {} by A1, Th51;
then A6: y `3 in A3 ;
A1 <> {} by A1, Th51;
then y `1 in A1 ;
hence ( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 ) by A2, A6, A5, A4, A3, Th72; :: thesis: verum