let F be Ternary-Field; :: thesis: for a, x, b, x9 being Scalar of F st a <> 0. F & Tern x,a,b = Tern x9,a,b holds
x = x9
let a, x, b, x9 be Scalar of F; :: thesis: ( a <> 0. F & Tern x,a,b = Tern x9,a,b implies x = x9 )
assume A1: ( a <> 0. F & Tern x,a,b = Tern x9,a,b ) ; :: thesis: x = x9
( Tern x,(0. F),b = b & Tern x9,(0. F),b = b ) by Def7;
hence x = x9 by A1, Def7; :: thesis: verum