let a, b be set ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in field R & a <> b holds
not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in field R & a <> b implies not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic )
assume A1: ( R is well-ordering & a in field R & b in field R & a <> b ) ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
then A2: R is connected by Def4;

A3: now

assume A4: R -Seg a c= R -Seg b ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
set S = R |_2 (R -Seg b);
A5: field (R |_2 (R -Seg b)) = R -Seg b by A1, Th40;
A6: a in R -Seg b

proof

assume not a in R -Seg b ; :: thesis: contradiction
then not [a,b] in R by A1, Def1;
then [b,a] in R by A1, A2, Lm4;
then b in R -Seg a by A1, Def1;
hence contradiction by A4, Def1; :: thesis: verum

end;

then A7: R -Seg a = (R |_2 (R -Seg b)) -Seg a by A1, Th35;
A8: (R |_2 (R -Seg b)) |_2 (R -Seg a) = R |_2 (R -Seg a) by A4, Th29;
R |_2 (R -Seg b) is well-ordering by A1, Th32;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A5, A6, A7, A8, Th50, Th57; :: thesis: verum

end;

A9: now

assume A10: R -Seg b c= R -Seg a ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
set S = R |_2 (R -Seg a);
A11: field (R |_2 (R -Seg a)) = R -Seg a by A1, Th40;
A12: b in R -Seg a

proof

assume not b in R -Seg a ; :: thesis: contradiction
then not [b,a] in R by A1, Def1;
then [a,b] in R by A1, A2, Lm4;
then a in R -Seg b by A1, Def1;
hence contradiction by A10, Def1; :: thesis: verum

end;

then A13: R -Seg b = (R |_2 (R -Seg a)) -Seg b by A1, Th35;
(R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by A10, Th29;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A11, A12, A13, Th32, Th57; :: thesis: verum

end;

R -Seg a,R -Seg b are_c=-comparable by A1, Th33;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A3, A9, XBOOLE_0:def 9; :: thesis: verum