let M be Cardinal; :: thesis: M in nextcard M
card M in nextcard M by Def6;
hence M in nextcard M by Def5; :: thesis: verum