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

( 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