let n be Nat; :: thesis: ( n > 0 implies card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 )
assume A1: n > 0 ; :: thesis: card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1
then A2: n >= 0 + 1 by NAT_1:13;
A3: 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 A4: i < n -' 1 by NAT_1:45;
n >= 0 + 1 by A1, NAT_1:13;
then i < n - 1 by A4, XREAL_1:235;
hence i + 1 < n by XREAL_1:22; :: thesis: verum

end;

deffunc H₁( Element of NAT ) -> set = [($1 + 1),$1];
defpred S₁[ Element of NAT ] means $1 + 1 < n;
defpred S₂[ Element of NAT ] means $1 in n -' 1;
A5: for i being Element of NAT holds
( S₁[i] iff S₂[i] )

proof

let i be Element of NAT ; :: thesis: ( S₁[i] iff S₂[i] )
thus ( i + 1 < n implies i in n -' 1 ) :: thesis: ( S₂[i] implies S₁[i] )

proof

assume i + 1 < n ; :: thesis: i in n -' 1
then i < n - 1 by XREAL_1:22;
then i < n -' 1 by A2, XREAL_1:235;
hence i in n -' 1 by NAT_1:45; :: thesis: verum

end;

thus ( S₂[i] implies S₁[i] ) by A3; :: thesis: verum

end;

A6: { H₁(i) where i is Element of NAT : S₁[i] } = { H₁(i) where i is Element of NAT : S₂[i] } from FRAENKEL:sch 3(A5);
A7: n -' 1 c= NAT ;
A8: for d1, d2 being Element of NAT st H₁(d1) = H₁(d2) holds
d1 = d2 by ZFMISC_1:33;
n -' 1,{ H₁(i) where i is Element of NAT : i in n -' 1 } are_equipotent from FUNCT_7:sch 4(A7, A8);
hence card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = card (n -' 1) by A6, CARD_1:21
.= n -' 1 by CARD_1:def 5
.= n - 1 by A2, XREAL_1:235 ;
:: thesis: verum