let m, n be Nat; :: thesis: ( Seg n, Seg m are_equipotent implies n = m )
defpred S2[ Nat] means ex n being Nat st
( Seg n, Seg $1 are_equipotent & n <> $1 );
assume ( Seg n, Seg m are_equipotent & n <> m ) ; :: thesis: contradiction
then A1: ex m being Nat st S2[m] ;
consider m being Nat such that
A2: S2[m] and
A3: for k being Nat st S2[k] holds
m <= k from NAT_1:sch 5(A1);
 consider n being Nat such that
A4: Seg n, Seg m are_equipotent and
A5: n <> m by A2;
A6: ex f being Function st
( f is one-to-one & dom f = Seg n & rng f = Seg m ) by A4;
A7: now :: thesis: not m = 0
assume m = 0 ; :: thesis: contradiction
then Seg m = {} ;
then Seg m = Seg n by A6, RELAT_1:42;
hence contradiction by A5, Th6; :: thesis: verum
end;
then consider m1 being Nat such that
A8: m = m1 + 1 by NAT_1:6;
A9: now :: thesis: not n = 0
assume n = 0 ; :: thesis: contradiction
then Seg n = {} ;
then Seg m = Seg n by A6, RELAT_1:42;
hence contradiction by A5, Th6; :: thesis: verum
end;
then consider n1 being Nat such that
A10: n = n1 + 1 by NAT_1:6;
A11: n in Seg n by A9, Th3;
A12: m in Seg m by A7, Th3;
A13: not n1 + 1 <= n1 by NAT_1:13;
A14: not m1 + 1 <= m1 by NAT_1:13;
A15: not n in Seg n1 by A10, A13, Th1;
A16: not m in Seg m1 by A8, A14, Th1;
A17: (Seg n1) /\ {n} c= {}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg n1) /\ {n} or x in {} )
assume x in (Seg n1) /\ {n} ; :: thesis: x in {}
then ( x in Seg n1 & x in {n} ) by XBOOLE_0:def 4;
hence x in {} by A15, TARSKI:def 1; :: thesis: verum
end;
A18: (Seg m1) /\ {m} c= {}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg m1) /\ {m} or x in {} )
assume x in (Seg m1) /\ {m} ; :: thesis: x in {}
then ( x in Seg m1 & x in {m} ) by XBOOLE_0:def 4;
hence x in {} by A16, TARSKI:def 1; :: thesis: verum
end;
A19: Seg n = (Seg n1) \/ {n} by A10, Th9;
A20: Seg m = (Seg m1) \/ {m} by A8, Th9;
A21: (Seg n1) /\ {n} = {} by A17;
A22: (Seg m1) /\ {m} = {} by A18;
A23: ( (Seg n1) \ {n} = ((Seg n1) \/ {n}) \ {n} & Seg n1 misses {n} ) by A21, XBOOLE_1:40;
A24: ( (Seg m1) \ {m} = ((Seg m1) \/ {m}) \ {m} & Seg m1 misses {m} ) by A22, XBOOLE_1:40;
A25: (Seg n) \ {n} = Seg n1 by A19, A23, XBOOLE_1:83;
(Seg m) \ {m} = Seg m1 by A20, A24, XBOOLE_1:83;
hence contradiction by A3, A4, A5, A8, A10, A11, A12, A14, A25, CARD_1:34; :: thesis: verum