let n be Nat; :: thesis: nextcard (card n) = card (succ n)
reconsider sn = succ n as Nat ;
A1: for M being Cardinal st card (card n) in M holds
card (succ n) c= M

proof

A2: card n = n by Def2;
let M be Cardinal; :: thesis: ( card (card n) in M implies card (succ n) c= M )
assume card (card n) in M ; :: thesis: card (succ n) c= M
then succ n c= M by A2, ORDINAL1:21;
hence card (succ n) c= M by Def2; :: thesis: verum

end;

n in succ n by ORDINAL1:6;
then card n in card sn by Th42;
hence nextcard (card n) = card (succ n) by A1, Def3; :: thesis: verum