let a, b, c be set ; :: 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 A1: ( 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 ) ; :: thesis: ( S -Seg c c= S -Seg b & [c,b] in S )
set P = R |_2 (R -Seg a);
set Q = S |_2 (S -Seg b);
set T = S |_2 (S -Seg c);
set F1 = canonical_isomorphism_of R,(S |_2 (S -Seg b));
A2: canonical_isomorphism_of R,(S |_2 (S -Seg b)) is_isomorphism_of R,S |_2 (S -Seg b) by A1, Def9;
R -Seg a c= field R by Th13;
then A3: 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, A2, Th59;
consider d being set such that
A4: ( d in field (S |_2 (S -Seg b)) & (canonical_isomorphism_of R,(S |_2 (S -Seg b))) .: (R -Seg a) = (S |_2 (S -Seg b)) -Seg d ) by A1, A2, Th60;
A5: S -Seg b = field (S |_2 (S -Seg b)) by A1, Th40;
then A6: (S |_2 (S -Seg b)) -Seg d = S -Seg d by A1, A4, Th35;
S |_2 (S -Seg c),R |_2 (R -Seg a) are_isomorphic by A1, Th50;
then A7: S |_2 (S -Seg c),(S |_2 (S -Seg b)) |_2 ((S |_2 (S -Seg b)) -Seg d) are_isomorphic by A3, A4, Th52;
A8: rng (canonical_isomorphism_of R,(S |_2 (S -Seg b))) = S -Seg b by A2, A5, Def7;
then A9: (S |_2 (S -Seg b)) -Seg d c= S -Seg b by A4, RELAT_1:144;
A10: S |_2 (S -Seg c),S |_2 (S -Seg d) are_isomorphic by A4, A6, A7, A8, Th29, RELAT_1:144;
d in field S by A4, Th19;
hence S -Seg c c= S -Seg b by A1, A6, A9, A10, Th58; :: thesis: [c,b] in S
hence [c,b] in S by A1, Th37; :: thesis: verum