let L be non empty ZeroStr ; :: thesis: for a, b, c being Element of L holds deg <%c,b,a%> <= 2
let a, b, c be Element of L; :: thesis: deg <%c,b,a%> <= 2
(len <%c,b,a%>) - 1 <= 3 - 1 by qua2, XREAL_1:9;
hence deg <%c,b,a%> <= 2 by HURWITZ:def 2; :: thesis: verum