let a, b, c be object ; 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; ( 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
; ( 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; [c,b] in S
hence
[c,b] in S
by A2, A4, A5, Th29; verum