let A, B be Ordinal; :: thesis: ( card A in card B implies A in B )
assume that
A1: card A in card B and
A2: not A in B ; :: thesis: contradiction
not card B c= card A by A1, CARD_1:4;
hence contradiction by A2, CARD_1:11, ORDINAL1:16; :: thesis: verum