let X be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 <> {} ; :: thesis: 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 ; :: thesis: ( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )

thus a in Y by A6; :: thesis: for b being object st b in Y holds
[a,b] in R

let b be object ; :: thesis: ( b in Y implies [a,b] in R )
assume A8: b in Y ; :: thesis: [a,b] in R
then not b in R -Seg a by ;
then ( a = b or not [b,a] in R ) by Th1;
then ( a <> b implies [a,b] in R ) by ;
hence [a,b] in R by ; :: thesis: verum