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

proof

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

end;

hence nextcard (card n) = card (succ n) by A1, Def6; :: thesis: verum