let F be Ternary-Field; :: thesis: for a, a9, u, u9, v, v9 being Scalar of F st a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) holds
( u = u9 & v = v9 )
let a, a9, u, u9, v, v9 be Scalar of F; :: thesis: ( a <> a9 & Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) implies ( u = u9 & v = v9 ) )
assume that
A1: a <> a9 and
A2: Tern (u,a,v) = Tern (u9,a,v9) and
A3: Tern (u,a9,v) = Tern (u9,a9,v9) ; :: thesis: ( u = u9 & v = v9 )
u = u9 by A1, A2, A3, Def5;
hence ( u = u9 & v = v9 ) by A2, Def5; :: thesis: verum