thus len <*x,y,z*> = 3 by FINSEQ_1:62; :: according to CIRCCOMB:def 12 :: thesis: verum