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