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 that
A1: R is well-ordering and
A2: ( a in field R & b in field R ) and
A3: a <> b ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
A4: R is connected by A1, Def4;

A5: now

set S = R |_2 (R -Seg a);
assume A6: R -Seg b c= R -Seg a ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
then A7: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th29;
A8: field (R |_2 (R -Seg a)) = R -Seg a by A1, Th40;
A9: b in R -Seg a

proof

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

end;

then R -Seg b = (R |_2 (R -Seg a)) -Seg b by A1, Th35;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A8, A9, A7, Th32, Th57; :: thesis: verum

end;

A10: now

set S = R |_2 (R -Seg b);
assume A11: R -Seg a c= R -Seg b ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
then A12: (R |_2 (R -Seg b)) |_2 (R -Seg a) = R |_2 (R -Seg a) by Th29;
A13: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th32, Th40;
A14: a in R -Seg b

proof

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

end;

then R -Seg a = (R |_2 (R -Seg b)) -Seg a by A1, Th35;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A14, A12, A13, Th50, 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 A10, A5, XBOOLE_0:def 9; :: thesis: verum