let Y be set ; :: thesis: for R being Relation st R is well-ordering & Y c= field R holds
( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )
let R be Relation; :: thesis: ( R is well-ordering & Y c= field R implies ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ) )
assume A1: ( R is well-ordering & Y c= field R ) ; :: thesis: ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )
then A2: R is transitive by Def4;
A3: R is antisymmetric by A1, Def4;

now

given a being set such that A4: ( a in field R & Y = R -Seg a ) ; :: thesis: for b being set st b in Y holds
for c being set st [c,b] in R holds
c in Y
let b be set ; :: thesis: ( b in Y implies for c being set st [c,b] in R holds
c in Y )
assume A5: b in Y ; :: thesis: for c being set st [c,b] in R holds
c in Y
let c be set ; :: thesis: ( [c,b] in R implies c in Y )
assume A6: [c,b] in R ; :: thesis: c in Y
A7: ( [b,a] in R & b <> a ) by A4, A5, Def1;
then A8: ( [c,a] in R & a in field R ) by A2, A6, Lm2, RELAT_1:30;
c <> a by A3, A6, A7, Lm3;
hence c in Y by A4, A8, Def1; :: thesis: verum

end;

hence ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) implies for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ) by RELAT_1:30; :: thesis: ( ex a being set st
( a in Y & ex b being set st
( [b,a] in R & not b in Y ) ) or Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) )
A9: R is connected by A1, Def4;
assume A10: for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ; :: thesis: ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) )
assume Y <> field R ; :: thesis: ex a being set st
( a in field R & Y = R -Seg a )
then consider d being set such that
A11: ( ( d in field R & not d in Y ) or ( d in Y & not d in field R ) ) by TARSKI:2;
(field R) \ Y <> {} by A1, A11, XBOOLE_0:def 5;
then consider a being set such that
A12: ( a in (field R) \ Y & ( for b being set st b in (field R) \ Y holds
[a,b] in R ) ) by A1, Th10;
take a ; :: thesis: ( a in field R & Y = R -Seg a )
thus a in field R by A12; :: thesis: Y = R -Seg a
thus Y = R -Seg a :: thesis: verum

proof

A13: now

let b be set ; :: thesis: ( b in Y implies b in R -Seg a )
assume A14: b in Y ; :: thesis: b in R -Seg a
assume not b in R -Seg a ; :: thesis: contradiction
then A15: ( not [b,a] in R or a = b ) by Def1;
A16: not a in Y by A12, XBOOLE_0:def 5;
a <> b by A12, A14, XBOOLE_0:def 5;
then [a,b] in R by A1, A9, A12, A14, A15, Lm4;
hence contradiction by A10, A14, A16; :: thesis: verum

end;

now

let b be set ; :: thesis: ( b in R -Seg a implies b in Y )
assume b in R -Seg a ; :: thesis: b in Y
then A17: ( [b,a] in R & b <> a ) by Def1;
then A18: b in field R by RELAT_1:30;
assume not b in Y ; :: thesis: contradiction
then b in (field R) \ Y by A18, XBOOLE_0:def 5;
then [a,b] in R by A12;
hence contradiction by A3, A17, Lm3; :: thesis: verum

end;

hence Y = R -Seg a by A13, TARSKI:2; :: thesis: verum

end;