let z be object ; :: thesis: for A, B, C being set st z in [:A,B,C:] holds
( z `1_3 in A & z `2_3 in B & z `3_3 in C )
let A, B, C be set ; :: thesis: ( z in [:A,B,C:] implies ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) )
assume A1: z in [:A,B,C:] ; :: thesis: ( z `1_3 in A & z `2_3 in B & z `3_3 in C )
then A2: not C is empty by MCART_1:31;
A3: ( not A is empty & not B is empty ) by A1, MCART_1:31;
then consider a being Element of A, b being Element of B, c being Element of C such that
A4: z = [a,b,c] by A1, A2, DOMAIN_1:3;
A5: z `3_3 = c by A4;
( z `1_3 = a & z `2_3 = b ) by A4;
hence ( z `1_3 in A & z `2_3 in B & z `3_3 in C ) by A3, A2, A5; :: thesis: verum