let z be object ; 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 ; ( 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:]
; ( 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; verum