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