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