thus card <%x,y%> = 2 by Th38; :: according to CARD_1:def 7 :: thesis: verum