thus card <%x%> = 1 by Th33; :: according to CARD_1:def 7 :: thesis: verum