let n be Nat; :: thesis: nextcard (card (Segm n)) = card (Segm (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A1: for M being Cardinal st card (card n) in M holds
card (n + 1) c= M

proof

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

end;

n < n + 1 by Th13;
hence nextcard (card (Segm n)) = card (Segm (n + 1)) by A1, Th29, CARD_1:def 3; :: thesis: verum