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
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
proof
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 R -Seg b = (R |_2 (R -Seg a)) -Seg b by A1, Th27;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A7, A8, A6, Th25, Th46; :: thesis: verum
end;
A9: now :: thesis: ( R -Seg a c= R -Seg b implies not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic )
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
proof
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 R -Seg a = (R |_2 (R -Seg b)) -Seg a by A1, Th27;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A13, A11, A12, Th40, Th46; :: thesis: verum
end;
R -Seg a,R -Seg b are_c=-comparable by A1, Th26;
hence not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A9, A4; :: thesis: verum