let n be Nat; :: thesis: ( n > 0 implies card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 )
deffunc H₁( Element of NAT ) -> object = [($1 + 1),$1];
defpred S₁[ Element of NAT ] means $1 + 1 < n;
defpred S₂[ Element of NAT ] means $1 in Segm (n -' 1);
A1: for d1, d2 being Element of NAT st H₁(d1) = H₁(d2) holds
d1 = d2 by XTUPLE_0:1;
assume A2: n > 0 ; :: thesis: card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = 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
( 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 Segm (n -' 1) ) :: thesis: ( S₂[i] implies S₁[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 ( S₂[i] implies S₁[i] ) by A4; :: thesis: verum

end;

A7: { H₁(i) where i is Element of NAT : S₁[i] } = { H₁(i) where i is Element of NAT : S₂[i] } from FRAENKEL:sch 3(A6);
A8: n -' 1 c= NAT ;
n -' 1, { H₁(i) where i is Element of NAT : i in n -' 1 } are_equipotent from FUNCT_7:sch 4(A8, A1);
hence card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = card (n -' 1) by A7, CARD_1:5
.= n -' 1
.= n - 1 by A3, XREAL_1:233 ;
:: thesis: verum