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 that
A1: R is well-ordering and
A2: 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 )
A3: R is antisymmetric by A1, Def4;
A4: R is transitive by A1, Def4;

now

given a being set such that a in field R and
A5: 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 A6: b in Y ; :: thesis: for c being set st [c,b] in R holds
c in Y
A7: [b,a] in R by A5, A6, Def1;
let c be set ; :: thesis: ( [c,b] in R implies c in Y )
assume A8: [c,b] in R ; :: thesis: c in Y
A9: [c,a] in R by A4, A8, A7, Lm2;
b <> a by A5, A6, Def1;
then c <> a by A3, A8, A7, Lm3;
hence c in Y by A5, A9, 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 ) )
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 not for d being set holds
( d in field R iff d in Y ) by TARSKI:2;
then (field R) \ Y <> {} by A2, XBOOLE_0:def 5;
then consider a being set such that
A11: a in (field R) \ Y and
A12: for b being set st b in (field R) \ Y holds
[a,b] in R by A1, Th10;

A13: now

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

end;

take a ; :: thesis: ( a in field R & Y = R -Seg a )
thus a in field R by A11; :: thesis: Y = R -Seg a
A18: R is connected by A1, Def4;

now

A19: not a in Y by A11, XBOOLE_0:def 5;
let b be set ; :: thesis: ( b in Y implies b in R -Seg a )
assume A20: b in Y ; :: thesis: b in R -Seg a
assume not b in R -Seg a ; :: thesis: contradiction
then A21: ( not [b,a] in R or a = b ) by Def1;
a <> b by A11, A20, XBOOLE_0:def 5;
then [a,b] in R by A2, A18, A11, A20, A21, Lm4;
hence contradiction by A10, A20, A19; :: thesis: verum

end;

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