theorem :: ALGSTR_3:5

for F being Ternary-Field
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