let L be non empty ZeroStr ; :: thesis: for a, b, c being Element of L holds
( deg <%c,b,a%> = 2 iff a <> 0. L )
let a, b, c be Element of L; :: thesis: ( deg <%c,b,a%> = 2 iff a <> 0. L )
H: deg <%c,b,a%> = (len <%c,b,a%>) - 1 by HURWITZ:def 2;

A: now :: thesis: ( a <> 0. L implies deg <%c,b,a%> = 2 )

assume a <> 0. L ; :: thesis: deg <%c,b,a%> = 2
then len <%c,b,a%> = 3 by qua3;
hence deg <%c,b,a%> = 2 by H; :: thesis: verum

end;

now :: thesis: ( deg <%c,b,a%> = 2 implies a <> 0. L )

assume deg <%c,b,a%> = 2 ; :: thesis: a <> 0. L
then len <%c,b,a%> = 2 + 1 by H;
then <%c,b,a%> . 2 <> 0. L by ALGSEQ_1:10;
hence a <> 0. L by qua1; :: thesis: verum

end;

hence ( deg <%c,b,a%> = 2 iff a <> 0. L ) by A; :: thesis: verum