let n be Nat; :: thesis: Seg n,n are_equipotent
defpred S₂[ Nat] means Seg $1,$1 are_equipotent ;
A1: S₂[ 0 ] ;
A2: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A3: Seg n,n are_equipotent ; :: thesis: S₂[n + 1]
A4: n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def 1 ;
A5: ( Seg (n + 1) = (Seg n) \/ {(n + 1)} & {(n + 1)},{n} are_equipotent ) by Th11, CARD_1:28;

A6: now

assume n meets {n} ; :: thesis: contradiction
then consider x being set such that
A7: x in n and
A8: x in {n} by XBOOLE_0:3;
x = n by A8, TARSKI:def 1;
hence contradiction by A7; :: thesis: verum

end;

now

assume Seg n meets {(n + 1)} ; :: thesis: contradiction
then consider x being set such that
A9: x in Seg n and
A10: x in {(n + 1)} by XBOOLE_0:3;
A11: x = n + 1 by A10, TARSKI:def 1;
not n + 1 <= n by NAT_1:13;
hence contradiction by A9, A11, Th3; :: thesis: verum

end;

hence S₂[n + 1] by A3, A4, A5, A6, CARD_1:31; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2);
hence Seg n,n are_equipotent ; :: thesis: verum