let M be Cardinal; :: thesis: M in nextcard M
( card M in nextcard M & M = card M ) by Def5, Def6;
hence M in nextcard M ; :: thesis: verum