n = len (x | n) ;
hence x | n is n -element by CARD_1:def 7; :: thesis: verum