theorem qua4: :: FIELD_9:18
for L being non empty ZeroStr
for a, b, c being Element of L holds
( deg <%c,b,a%> = 2 iff a <> 0. L )