let n, m be Nat; :: thesis: ( Seg n, Seg m are_equipotent implies n = m )
defpred S₂[ 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 S₂[m] ;
consider m being Nat such that
A2: S₂[m] and
A3: for k being Nat st S₂[k] holds
m <= k from NAT_1:sch 5(A1);
consider n being Nat such that
A4: ( Seg n, Seg m are_equipotent & n <> m ) by A2;
A5: ex f being Function st
( f is one-to-one & dom f = Seg n & rng f = Seg m ) by A4, WELLORD2:def 4;

A6: now

assume m = 0 ; :: thesis: contradiction
then Seg m = Seg n by A5, Th4, RELAT_1:65;
hence contradiction by A4, Th8; :: thesis: verum

end;

then consider m1 being Nat such that
A7: m = m1 + 1 by NAT_1:6;

A8: now

assume n = 0 ; :: thesis: contradiction
then Seg m = Seg n by A5, Th4, RELAT_1:65;
hence contradiction by A4, Th8; :: thesis: verum

end;

then consider n1 being Nat such that
A9: n = n1 + 1 by NAT_1:6;
reconsider m1 = m1, n1 = n1 as Element of NAT by ORDINAL1:def 13;
A10: ( n in Seg n & m in Seg m ) by A6, A8, Th5;
A11: ( not n1 + 1 <= n1 & not m1 + 1 <= m1 ) by NAT_1:13;
then A12: ( not n in Seg n1 & not m in Seg m1 ) by A7, A9, Th3;
A13: (Seg n1) /\ {n} c= {}

proof

let x be set ; :: 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 A12, TARSKI:def 1; :: thesis: verum

end;

(Seg m1) /\ {m} c= {}

proof

let x be set ; :: 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 A12, TARSKI:def 1; :: thesis: verum

end;

then A14: ( Seg n = (Seg n1) \/ {n} & Seg m = (Seg m1) \/ {m} & (Seg n1) \ {n} = ((Seg n1) \/ {n}) \ {n} & (Seg m1) \ {m} = ((Seg m1) \/ {m}) \ {m} & (Seg n1) /\ {n} = {} & (Seg m1) /\ {m} = {} ) by A7, A9, A13, Th11, XBOOLE_1:40;
then ( Seg n1 misses {n} & Seg m1 misses {m} ) by XBOOLE_0:def 7;
then ( (Seg n) \ {n} = Seg n1 & (Seg m) \ {m} = Seg m1 ) by A14, XBOOLE_1:83;
hence contradiction by A3, A4, A7, A9, A10, A11, CARD_1:61; :: thesis: verum