thus len <*x,y*> = 2 by Th61; :: according to CARD_1:def 7 :: thesis: verum