let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (n -SuccRelStr) = n - 1 )
deffunc H1( Element of NAT ) -> object = [$1,($1 + 1)];
defpred S1[ Element of NAT ] means $1 + 1 < n;
defpred S2[ set ] means $1 in Segm (n -' 1);
A1: n -' 1 c= NAT ;
assume A2: n > 0 ; :: thesis: card the InternalRel of (n -SuccRelStr) = n - 1
then A3: n >= 0 + 1 by NAT_1:13;
A4: for i being Nat st i in Segm (n -' 1) holds
i + 1 < n
proof
let i be Nat; :: thesis: ( i in Segm (n -' 1) implies i + 1 < n )
assume i in Segm (n -' 1) ; :: thesis: i + 1 < n
then A5: i < n -' 1 by NAT_1:44;
n >= 0 + 1 by A2, NAT_1:13;
then i < n - 1 by A5, XREAL_1:233;
hence i + 1 < n by XREAL_1:20; :: thesis: verum
end;
A6: for i being Element of NAT holds
( S1[i] iff S2[i] )
proof
let i be Element of NAT ; :: thesis: ( S1[i] iff S2[i] )
thus ( i + 1 < n implies i in Segm (n -' 1) ) :: thesis: ( S2[i] implies S1[i] )
proof
assume i + 1 < n ; :: thesis: i in Segm (n -' 1)
then i < n - 1 by XREAL_1:20;
then i < n -' 1 by A3, XREAL_1:233;
hence i in Segm (n -' 1) by NAT_1:44; :: thesis: verum
end;
thus ( S2[i] implies S1[i] ) by A4; :: thesis: verum
end;
A7: { H1(i) where i is Element of NAT : S1[i] } = { H1(i) where i is Element of NAT : S2[i] } from FRAENKEL:sch 3(A6);
 deffunc H2( Element of NAT ) -> object = [$1,($1 + 1)];
A8: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 by XTUPLE_0:1;
A9: n -' 1, { H2(i) where i is Element of NAT : i in n -' 1 } are_equipotent from FUNCT_7:sch 4(A1, A8);
 thus card the InternalRel of (n -SuccRelStr) = card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by Def6
.= card (n -' 1) by A7, A9, CARD_1:5
.= n -' 1
.= n - 1 by A3, XREAL_1:233 ; :: thesis: verum