let n be Nat; :: thesis: Seg n,n are_equipotent
defpred S2[ Nat] means Seg $1,$1 are_equipotent ;
A1: S2[ 0 ] by Th4;
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: Seg (n + 1) = (Seg n) \/ {(n + 1)} by Th11;
A5: n + 1 = succ n by NAT_1:39
.= n \/ {n} by ORDINAL1:def 1 ;
A6: {(n + 1)},{n} are_equipotent by CARD_1:48;
A7: now
assume n meets {n} ; :: thesis: contradiction
then consider x being set such that
A8: ( x in n & x in {n} ) by XBOOLE_0:3;
x = n by A8, TARSKI:def 1;
hence contradiction by A8; :: thesis: verum
end;
now
assume Seg n meets {(n + 1)} ; :: thesis: contradiction
then consider x being set such that
A9: ( x in Seg n & x in {(n + 1)} ) by XBOOLE_0:3;
A10: ( x = n + 1 & n <= n ) by A9, TARSKI:def 1;
not n + 1 <= n by NAT_1:13;
hence contradiction by A9, A10, Th3; :: thesis: verum
end;
hence S2[n + 1] by A3, A4, A5, A6, A7, CARD_1:58; :: 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