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

proof

A2: card n = n by Def5;
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:33;
hence card (succ n) c= M by Def5; :: thesis: verum

end;

n in succ n by ORDINAL1:10;
then card n in card sn by Th73;
hence nextcard (card n) = card (succ n) by A1, Def6; :: thesis: verum