let a, b be object ; :: 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

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A9, A4; :: thesis: verum

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: now :: thesis: ( R -Seg b c= R -Seg a implies not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic )

set S = R |_2 (R -Seg a);

assume A5: R -Seg b c= R -Seg a ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic

then A6: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;

A7: field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

A8: b in R -Seg a

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A7, A8, A6, Th25, Th46; :: thesis: verum

end;assume A5: R -Seg b c= R -Seg a ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic

then A6: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;

A7: field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

A8: b in R -Seg a

proof

then
R -Seg b = (R |_2 (R -Seg a)) -Seg b
by A1, Th27;
assume
not b in R -Seg a
; :: thesis: contradiction

then not [b,a] in R by A3, Th1;

then [a,b] in R by A2, A3, A1, Lm4;

then a in R -Seg b by A3, Th1;

hence contradiction by A5, Th1; :: thesis: verum

end;then not [b,a] in R by A3, Th1;

then [a,b] in R by A2, A3, A1, Lm4;

then a in R -Seg b by A3, Th1;

hence contradiction by A5, Th1; :: thesis: verum

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A7, A8, A6, Th25, Th46; :: thesis: verum

A9: now :: thesis: ( R -Seg a c= R -Seg b implies not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic )

R -Seg a,R -Seg b are_c=-comparable
by A1, Th26;set S = R |_2 (R -Seg b);

assume A10: R -Seg a c= R -Seg b ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic

then A11: (R |_2 (R -Seg b)) |_2 (R -Seg a) = R |_2 (R -Seg a) by Th22;

A12: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;

A13: a in R -Seg b

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A13, A11, A12, Th40, Th46; :: thesis: verum

end;assume A10: R -Seg a c= R -Seg b ; :: thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic

then A11: (R |_2 (R -Seg b)) |_2 (R -Seg a) = R |_2 (R -Seg a) by Th22;

A12: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;

A13: a in R -Seg b

proof

then
R -Seg a = (R |_2 (R -Seg b)) -Seg a
by A1, Th27;
assume
not a in R -Seg b
; :: thesis: contradiction

then not [a,b] in R by A3, Th1;

then [b,a] in R by A2, A3, A1, Lm4;

then b in R -Seg a by A3, Th1;

hence contradiction by A10, Th1; :: thesis: verum

end;then not [a,b] in R by A3, Th1;

then [b,a] in R by A2, A3, A1, Lm4;

then b in R -Seg a by A3, Th1;

hence contradiction by A10, Th1; :: thesis: verum

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A13, A11, A12, Th40, Th46; :: thesis: verum

hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A9, A4; :: thesis: verum