thus len <*x,y,z*> = 3 by Th62; :: according to CARD_1:def 7 :: thesis: verum