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 object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object 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 object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object 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 object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y )

( a in field R & Y = R -Seg a ) ) implies for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y ) by RELAT_1:15; :: thesis: ( ex a being object st

( a in Y & ex b being object st

( [b,a] in R & not b in Y ) ) or Y = field R or ex a being object st

( a in field R & Y = R -Seg a ) )

assume A8: for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y ; :: thesis: ( Y = field R or ex a being object st

( a in field R & Y = R -Seg a ) )

assume Y <> field R ; :: thesis: ex a being object st

( a in field R & Y = R -Seg a )

then not for d being object 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 object such that

A9: a in (field R) \ Y and

A10: for b being object st b in (field R) \ Y holds

[a,b] in R by A1, Th6;

thus a in field R by A9; :: thesis: Y = R -Seg a

( ( Y = field R or ex a being object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object 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 object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object 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 object st

( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y )

now :: thesis: ( ex a being object st

( a in field R & Y = R -Seg a ) implies for b being object st b in Y holds

for c being object st [c,b] in R holds

c in Y )

hence
( ( Y = field R or ex a being object st ( a in field R & Y = R -Seg a ) implies for b being object st b in Y holds

for c being object st [c,b] in R holds

c in Y )

given a being object such that
a in field R
and

A3: Y = R -Seg a ; :: thesis: for b being object st b in Y holds

for c being object st [c,b] in R holds

c in Y

let b be object ; :: thesis: ( b in Y implies for c being object st [c,b] in R holds

c in Y )

assume A4: b in Y ; :: thesis: for c being object st [c,b] in R holds

c in Y

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

let c be object ; :: thesis: ( [c,b] in R implies c in Y )

assume A6: [c,b] in R ; :: thesis: c in Y

A7: [c,a] in R by A1, A6, A5, Lm2;

b <> a by A3, A4, Th1;

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

hence c in Y by A3, A7, Th1; :: thesis: verum

end;A3: Y = R -Seg a ; :: thesis: for b being object st b in Y holds

for c being object st [c,b] in R holds

c in Y

let b be object ; :: thesis: ( b in Y implies for c being object st [c,b] in R holds

c in Y )

assume A4: b in Y ; :: thesis: for c being object st [c,b] in R holds

c in Y

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

let c be object ; :: thesis: ( [c,b] in R implies c in Y )

assume A6: [c,b] in R ; :: thesis: c in Y

A7: [c,a] in R by A1, A6, A5, Lm2;

b <> a by A3, A4, Th1;

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

hence c in Y by A3, A7, Th1; :: thesis: verum

( a in field R & Y = R -Seg a ) ) implies for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y ) by RELAT_1:15; :: thesis: ( ex a being object st

( a in Y & ex b being object st

( [b,a] in R & not b in Y ) ) or Y = field R or ex a being object st

( a in field R & Y = R -Seg a ) )

assume A8: for a being object st a in Y holds

for b being object st [b,a] in R holds

b in Y ; :: thesis: ( Y = field R or ex a being object st

( a in field R & Y = R -Seg a ) )

assume Y <> field R ; :: thesis: ex a being object st

( a in field R & Y = R -Seg a )

then not for d being object 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 object such that

A9: a in (field R) \ Y and

A10: for b being object st b in (field R) \ Y holds

[a,b] in R by A1, Th6;

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

b in Y

take
a
; :: thesis: ( a in field R & Y = R -Seg a )b in Y

let b be object ; :: thesis: ( b in R -Seg a implies b in Y )

assume A12: b in R -Seg a ; :: thesis: b in Y

then A13: [b,a] in R by Th1;

assume A14: not b in Y ; :: thesis: contradiction

b in field R by A13, RELAT_1:15;

then b in (field R) \ Y by A14, XBOOLE_0:def 5;

then A15: [a,b] in R by A10;

b <> a by A12, Th1;

hence contradiction by A1, A13, A15, Lm3; :: thesis: verum

end;assume A12: b in R -Seg a ; :: thesis: b in Y

then A13: [b,a] in R by Th1;

assume A14: not b in Y ; :: thesis: contradiction

b in field R by A13, RELAT_1:15;

then b in (field R) \ Y by A14, XBOOLE_0:def 5;

then A15: [a,b] in R by A10;

b <> a by A12, Th1;

hence contradiction by A1, A13, A15, Lm3; :: thesis: verum

thus a in field R by A9; :: thesis: Y = R -Seg a

now :: thesis: for b being object st b in Y holds

b in R -Seg a

hence
Y = R -Seg a
by A11, TARSKI:2; :: thesis: verumb in R -Seg a

A16:
not a in Y
by A9, XBOOLE_0:def 5;

let b be object ; :: thesis: ( b in Y implies b in R -Seg a )

assume A17: b in Y ; :: thesis: b in R -Seg a

assume not b in R -Seg a ; :: thesis: contradiction

then A18: ( not [b,a] in R or a = b ) by Th1;

a <> b by A9, A17, XBOOLE_0:def 5;

then [a,b] in R by A2, A1, A9, A17, A18, Lm4;

hence contradiction by A8, A17, A16; :: thesis: verum

end;let b be object ; :: thesis: ( b in Y implies b in R -Seg a )

assume A17: b in Y ; :: thesis: b in R -Seg a

assume not b in R -Seg a ; :: thesis: contradiction

then A18: ( not [b,a] in R or a = b ) by Th1;

a <> b by A9, A17, XBOOLE_0:def 5;

then [a,b] in R by A2, A1, A9, A17, A18, Lm4;

hence contradiction by A8, A17, A16; :: thesis: verum