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: Segm (n + 1) = succ (Segm n) by NAT_1:38
.= n \/ {n} ;
A5: ( Seg (n + 1) = (Seg n) \/ {(n + 1)} & {(n + 1)},{n} are_equipotent ) by Th9, CARD_1:28;

A6: now :: thesis: not n meets {n}

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

end;

now :: thesis: not Seg n meets {(n + 1)}

assume Seg n meets {(n + 1)} ; :: thesis: contradiction
then consider x being object 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, Th1; :: 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