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