let a, b, c be object ; :: thesis: for R, S being Relation st R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic holds
( S -Seg c c= S -Seg b & [c,b] in S )
let R, S be Relation; :: thesis: ( R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic implies ( S -Seg c c= S -Seg b & [c,b] in S ) )
assume that
A1: R is well-ordering and
A2: S is well-ordering and
A3: a in field R and
A4: b in field S and
A5: c in field S and
A6: R,S |_2 (S -Seg b) are_isomorphic and
A7: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ; :: thesis: ( S -Seg c c= S -Seg b & [c,b] in S )
set Q = S |_2 (S -Seg b);
set F1 = canonical_isomorphism_of (R,(S |_2 (S -Seg b)));
A8: canonical_isomorphism_of (R,(S |_2 (S -Seg b))) is_isomorphism_of R,S |_2 (S -Seg b) by A1, A6, Def9;
then consider d being object such that
A9: d in field (S |_2 (S -Seg b)) and
A10: (canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) .: (R -Seg a) = (S |_2 (S -Seg b)) -Seg d by A3, Th49;
A11: S -Seg b = field (S |_2 (S -Seg b)) by A2, Th32;
then A12: (S |_2 (S -Seg b)) -Seg d = S -Seg d by A2, A9, Th27;
A13: rng (canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) = S -Seg b by A8, A11;
then A14: (S |_2 (S -Seg b)) -Seg d c= S -Seg b by A10, RELAT_1:111;
set T = S |_2 (S -Seg c);
set P = R |_2 (R -Seg a);
A15: S |_2 (S -Seg c),R |_2 (R -Seg a) are_isomorphic by A7, Th40;
A16: d in field S by A9, Th12;
R -Seg a c= field R by Th9;
then R |_2 (R -Seg a),(S |_2 (S -Seg b)) |_2 ((canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) .: (R -Seg a)) are_isomorphic by A1, A8, Th48;
then S |_2 (S -Seg c),(S |_2 (S -Seg b)) |_2 ((S |_2 (S -Seg b)) -Seg d) are_isomorphic by A10, A15, Th42;
then S |_2 (S -Seg c),S |_2 (S -Seg d) are_isomorphic by A10, A12, A13, Th22, RELAT_1:111;
hence S -Seg c c= S -Seg b by A2, A5, A12, A14, A16, Th47; :: thesis: [c,b] in S
hence [c,b] in S by A2, A4, A5, Th29; :: thesis: verum