let n be Nat; :: thesis: Seg n,n are_equipotent
defpred S2[ Nat] means Seg $1,$1 are_equipotent ;
A1: S2[ 0 ] ;
A2: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A3: Seg n,n are_equipotent ; :: thesis: S2[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;
A: x = n by A8, TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A7, A; :: 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 S2[n + 1] by A3, A4, A5, A6, CARD_1:31; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A1, A2);
 hence Seg n,n are_equipotent ; :: thesis: verum