let Y be set ; 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; ( 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
; ( ( 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 ( 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
;
for b being object st b in Y holds
for c being object st [c,b] in R holds
c in Ylet b be
object ;
( b in Y implies for c being object st [c,b] in R holds
c in Y )assume A4:
b in Y
;
for c being object st [c,b] in R holds
c in YA5:
[b,a] in R
by A3, A4, Th1;
let c be
object ;
( [c,b] in R implies c in Y )assume A6:
[c,b] in R
;
c in YA7:
[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;
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; ( 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
; ( Y = field R or ex a being object st
( a in field R & Y = R -Seg a ) )
assume
Y <> field R
; 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;
take
a
; ( a in field R & Y = R -Seg a )
thus
a in field R
by A9; Y = R -Seg a
now for b being object st b in Y holds
b in R -Seg aA16:
not
a in Y
by A9, XBOOLE_0:def 5;
let b be
object ;
( b in Y implies b in R -Seg a )assume A17:
b in Y
;
b in R -Seg aassume
not
b in R -Seg a
;
contradictionthen 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;
verum end;
hence
Y = R -Seg a
by A11, TARSKI:2; verum