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 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, WELLORD2:def 4;

A7: now

assume m = 0 ; :: thesis: contradiction
then Seg m = {} ;
then Seg m = Seg n by A6, RELAT_1:65;
hence contradiction by A5, Th8; :: thesis: verum

end;

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

A9: now

assume n = 0 ; :: thesis: contradiction
then Seg n = {} ;
then Seg m = Seg n by A6, RELAT_1:65;
hence contradiction by A5, Th8; :: thesis: verum

end;

then consider n1 being Nat such that
A10: n = n1 + 1 by NAT_1:6;
reconsider m1 = m1, n1 = n1 as Element of NAT by ORDINAL1:def 13;
A11: n in Seg n by A9, Th5;
A12: m in Seg m by A7, Th5;
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, Th3;
A16: not m in Seg m1 by A8, A14, Th3;
A17: (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 A15, TARSKI:def 1; :: thesis: verum

end;

A18: (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 A16, TARSKI:def 1; :: thesis: verum

end;

A19: Seg n = (Seg n1) \/ {n} by A10, Th11;
A20: Seg m = (Seg m1) \/ {m} by A8, Th11;
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_0:def 7, XBOOLE_1:40;
A24: ( (Seg m1) \ {m} = ((Seg m1) \/ {m}) \ {m} & Seg m1 misses {m} ) by A22, XBOOLE_0:def 7, 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:61; :: thesis: verum