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 )
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 )
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;
hence ( ( Y = field R or ex a being object st
( 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
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;
take a ; :: thesis: ( a in field R & Y = R -Seg a )
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
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;
hence Y = R -Seg a by A11, TARSKI:2; :: thesis: verum