let x, y, X, Y, Z be set ; :: thesis: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] & x in [:X,Y,Z:] implies x = y )
assume A1: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] ) ; :: thesis: ( not x in [:X,Y,Z:] or x = y )
assume x in [:X,Y,Z:] ; :: thesis: x = y
hence x = [(x `1_3),(x `2_3),(x `3_3)] by Th3
.= y by A1, Th3 ;
:: thesis: verum