let a, b be set ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b
let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in R -Seg a implies (R |_2 (R -Seg a)) -Seg b = R -Seg b )
assume A1: ( R is well-ordering & a in field R & b in R -Seg a ) ; :: thesis: (R |_2 (R -Seg a)) -Seg b = R -Seg b
then A2: ( R is transitive & R is reflexive & R is antisymmetric ) by Def4;
set S = R |_2 (R -Seg a);

A3: now

let c be set ; :: thesis: ( c in (R |_2 (R -Seg a)) -Seg b implies c in R -Seg b )
assume c in (R |_2 (R -Seg a)) -Seg b ; :: thesis: c in R -Seg b
then A4: ( [c,b] in R |_2 (R -Seg a) & c <> b ) by Def1;
then [c,b] in R by XBOOLE_0:def 4;
hence c in R -Seg b by A4, Def1; :: thesis: verum

end;

now

let c be set ; :: thesis: ( c in R -Seg b implies c in (R |_2 (R -Seg a)) -Seg b )
assume c in R -Seg b ; :: thesis: c in (R |_2 (R -Seg a)) -Seg b
then A5: ( [c,b] in R & c <> b ) by Def1;
A6: ( [b,a] in R & b <> a ) by A1, Def1;
then A7: [c,a] in R by A2, A5, Lm2;
c <> a by A2, A5, A6, Lm3;
then c in R -Seg a by A7, Def1;
then [c,b] in [:(R -Seg a),(R -Seg a):] by A1, ZFMISC_1:106;
then [c,b] in R |_2 (R -Seg a) by A5, XBOOLE_0:def 4;
hence c in (R |_2 (R -Seg a)) -Seg b by A5, Def1; :: thesis: verum

end;

then ( R -Seg b c= (R |_2 (R -Seg a)) -Seg b & (R |_2 (R -Seg a)) -Seg b c= R -Seg b ) by A3, TARSKI:def 3;
hence (R |_2 (R -Seg a)) -Seg b = R -Seg b by XBOOLE_0:def 10; :: thesis: verum