let L be non empty ZeroStr ; :: thesis: for a, b, c being Element of L holds len <%c,b,a%> <= 3
let a, b, c be Element of L; :: thesis: len <%c,b,a%> <= 3
3 is_at_least_length_of <%c,b,a%> by qua1;
hence len <%c,b,a%> <= 3 by ALGSEQ_1:def 3; :: thesis: verum