let a, b be object ; :: thesis: for R being Relation st R is well-ordering & 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 & b in R -Seg a implies (R |_2 (R -Seg a)) -Seg b = R -Seg b )

assume that

A1: R is well-ordering and

A2: b in R -Seg a ; :: thesis: (R |_2 (R -Seg a)) -Seg b = R -Seg b

set S = R |_2 (R -Seg a);

hence (R |_2 (R -Seg a)) -Seg b = R -Seg b by A8; :: thesis: verum

(R |_2 (R -Seg a)) -Seg b = R -Seg b

let R be Relation; :: thesis: ( R is well-ordering & b in R -Seg a implies (R |_2 (R -Seg a)) -Seg b = R -Seg b )

assume that

A1: R is well-ordering and

A2: b in R -Seg a ; :: thesis: (R |_2 (R -Seg a)) -Seg b = R -Seg b

set S = R |_2 (R -Seg a);

now :: thesis: for c being object st c in R -Seg b holds

c in (R |_2 (R -Seg a)) -Seg b

then A8:
R -Seg b c= (R |_2 (R -Seg a)) -Seg b
;c in (R |_2 (R -Seg a)) -Seg b

let c be object ; :: thesis: ( c in R -Seg b implies c in (R |_2 (R -Seg a)) -Seg b )

assume A3: c in R -Seg b ; :: thesis: c in (R |_2 (R -Seg a)) -Seg b

then A4: [c,b] in R by Th1;

A5: [b,a] in R by A2, Th1;

then A6: [c,a] in R by A1, A4, Lm2;

A7: c <> b by A3, Th1;

then c <> a by A1, A4, A5, Lm3;

then c in R -Seg a by A6, Th1;

then [c,b] in [:(R -Seg a),(R -Seg a):] by A2, ZFMISC_1:87;

then [c,b] in R |_2 (R -Seg a) by A4, XBOOLE_0:def 4;

hence c in (R |_2 (R -Seg a)) -Seg b by A7, Th1; :: thesis: verum

end;assume A3: c in R -Seg b ; :: thesis: c in (R |_2 (R -Seg a)) -Seg b

then A4: [c,b] in R by Th1;

A5: [b,a] in R by A2, Th1;

then A6: [c,a] in R by A1, A4, Lm2;

A7: c <> b by A3, Th1;

then c <> a by A1, A4, A5, Lm3;

then c in R -Seg a by A6, Th1;

then [c,b] in [:(R -Seg a),(R -Seg a):] by A2, ZFMISC_1:87;

then [c,b] in R |_2 (R -Seg a) by A4, XBOOLE_0:def 4;

hence c in (R |_2 (R -Seg a)) -Seg b by A7, Th1; :: thesis: verum

now :: thesis: for c being object st c in (R |_2 (R -Seg a)) -Seg b holds

c in R -Seg b

then
(R |_2 (R -Seg a)) -Seg b c= R -Seg b
;c in R -Seg b

let c be object ; :: thesis: ( c in (R |_2 (R -Seg a)) -Seg b implies c in R -Seg b )

assume A9: c in (R |_2 (R -Seg a)) -Seg b ; :: thesis: c in R -Seg b

then [c,b] in R |_2 (R -Seg a) by Th1;

then A10: [c,b] in R by XBOOLE_0:def 4;

c <> b by A9, Th1;

hence c in R -Seg b by A10, Th1; :: thesis: verum

end;assume A9: c in (R |_2 (R -Seg a)) -Seg b ; :: thesis: c in R -Seg b

then [c,b] in R |_2 (R -Seg a) by Th1;

then A10: [c,b] in R by XBOOLE_0:def 4;

c <> b by A9, Th1;

hence c in R -Seg b by A10, Th1; :: thesis: verum

hence (R |_2 (R -Seg a)) -Seg b = R -Seg b by A8; :: thesis: verum