let X be set ; for R being Relation st R well_orders X holds
for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
let R be Relation; ( R well_orders X implies for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) ) )
assume A1:
R well_orders X
; for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
then A2:
R is_reflexive_in X
;
A3:
R is_connected_in X
by A1;
let Y be set ; ( Y c= X & Y <> {} implies ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) ) )
assume that
A4:
Y c= X
and
A5:
Y <> {}
; ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
R is_well_founded_in X
by A1;
then consider a being object such that
A6:
a in Y
and
A7:
R -Seg a misses Y
by A4, A5;
take
a
; ( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
thus
a in Y
by A6; for b being object st b in Y holds
[a,b] in R
let b be object ; ( b in Y implies [a,b] in R )
assume A8:
b in Y
; [a,b] in R
then
not b in R -Seg a
by A7, XBOOLE_0:3;
then
( a = b or not [b,a] in R )
by Th1;
then
( a <> b implies [a,b] in R )
by A3, A4, A6, A8, RELAT_2:def 6;
hence
[a,b] in R
by A2, A4, A6, RELAT_2:def 1; verum