let L be non empty ZeroStr ; :: thesis: for a, b, c being Element of L st a <> 0. L holds
len <%c,b,a%> = 3
let a, b, c be Element of L; :: thesis: ( a <> 0. L implies len <%c,b,a%> = 3 )
assume a <> 0. L ; :: thesis: len <%c,b,a%> = 3
then <%c,b,a%> . 2 <> 0. L by qua1;
then A1: for n being Nat st n is_at_least_length_of <%c,b,a%> holds
2 + 1 <= n by NAT_1:13;
3 is_at_least_length_of <%c,b,a%> by qua1;
hence len <%c,b,a%> = 3 by A1, ALGSEQ_1:def 3; :: thesis: verum