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