let L be non empty ZeroStr ; :: thesis: for z0, z1, z2 being Element of L holds len <%z0,z1,z2%> <= 3
let z0, z1, z2 be Element of L; :: thesis: len <%z0,z1,z2%> <= 3
3 is_at_least_length_of <%z0,z1,z2%> by Th24;
hence len <%z0,z1,z2%> <= 3 by ALGSEQ_1:def 3; :: thesis: verum