theorem Th25: :: NIVEN:27

for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds len <%z0,z1,z2%> <= 3