let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (n -SuccRelStr ) = n - 1 )
deffunc H1( Element of NAT ) -> set = [$1,($1 + 1)];
defpred S1[ Element of NAT ] means $1 + 1 < n;
defpred S2[ set ] means $1 in 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 n -' 1 holds
i + 1 < n
proof
let i be Nat; :: thesis: ( i in n -' 1 implies i + 1 < n )
assume i in n -' 1 ; :: thesis: i + 1 < n
then A5: i < n -' 1 by NAT_1:45;
n >= 0 + 1 by A2, NAT_1:13;
then i < n - 1 by A5, XREAL_1:235;
hence i + 1 < n by XREAL_1:22; :: 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 n -' 1 ) :: thesis: ( S2[i] implies S1[i] )
proof
assume i + 1 < n ; :: thesis: i in n -' 1
then i < n - 1 by XREAL_1:22;
then i < n -' 1 by A3, XREAL_1:235;
hence i in n -' 1 by NAT_1:45; :: 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 ) -> set = [$1,($1 + 1)];
A8: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 by ZFMISC_1:33;
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 Def7
.= card (n -' 1) by A7, A9, CARD_1:21
.= n -' 1 by CARD_1:def 5
.= n - 1 by A3, XREAL_1:235 ; :: thesis: verum