let a, b be triple object ; :: thesis: ( a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 implies a = b )
assume A1: ( a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 ) ; :: thesis: a = b
( a = [(a `1_3),(a `2_3),(a `3_3)] & b = [(b `1_3),(b `2_3),(b `3_3)] ) ;
hence a = b by A1; :: thesis: verum