let R be Relation; :: thesis: ( R is well-ordering implies for Y being set st Y c= field R & 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 is well-ordering ; :: thesis: for Y being set st Y c= field R & Y <> {} holds

ex a being object st

( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

let Y be set ; :: thesis: ( Y c= field R & 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

A2: Y c= field R and

A3: Y <> {} ; :: thesis: ex a being object st

( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

consider a being object such that

A4: a in Y and

A5: R -Seg a misses Y by A1, A2, A3, Def2;

take a ; :: thesis: ( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

thus a in Y by A4; :: 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 A6: b in Y ; :: thesis: [a,b] in R

then not b in R -Seg a by A5, XBOOLE_0:3;

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

then ( a <> b implies [a,b] in R ) by A1, A2, A4, A6, Lm4;

hence [a,b] in R by A1, A2, A4, Lm1; :: thesis: verum

ex a being object st

( a in Y & ( for b being object st b in Y holds

[a,b] in R ) ) )

assume A1: R is well-ordering ; :: thesis: for Y being set st Y c= field R & Y <> {} holds

ex a being object st

( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

let Y be set ; :: thesis: ( Y c= field R & 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

A2: Y c= field R and

A3: Y <> {} ; :: thesis: ex a being object st

( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

consider a being object such that

A4: a in Y and

A5: R -Seg a misses Y by A1, A2, A3, Def2;

take a ; :: thesis: ( a in Y & ( for b being object st b in Y holds

[a,b] in R ) )

thus a in Y by A4; :: 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 A6: b in Y ; :: thesis: [a,b] in R

then not b in R -Seg a by A5, XBOOLE_0:3;

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

then ( a <> b implies [a,b] in R ) by A1, A2, A4, A6, Lm4;

hence [a,b] in R by A1, A2, A4, Lm1; :: thesis: verum