let A be Element of omega ; :: thesis: A = x". (x. (card A))
A = card A by CARD_1:def 2;
hence A = x". (x. (card A)) by Def3; :: thesis: verum