let n, m be natural number ; :: thesis: ( card n in card m iff n in m )
card n = n by Def5;
hence ( card n in card m iff n in m ) by Def5; :: thesis: verum