let F be Ternary-Field; :: thesis: for a being Scalar of F st a <> 0. F holds
for b, c being Scalar of F ex x being Scalar of F st Tern a,x,b = c
let a be Scalar of F; :: thesis: ( a <> 0. F implies for b, c being Scalar of F ex x being Scalar of F st Tern a,x,b = c )
assume A1: a <> 0. F ; :: thesis: for b, c being Scalar of F ex x being Scalar of F st Tern a,x,b = c
let b, c be Scalar of F; :: thesis: ex x being Scalar of F st Tern a,x,b = c
consider x being Scalar of F such that
A2: Tern a,x,b = Tern (0. F),x,c by A1, Def7;
take x ; :: thesis: Tern a,x,b = c
thus Tern a,x,b = c by A2, Def7; :: thesis: verum