let R be Relation; :: thesis: ( R is well-ordering implies for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set 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 set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
then A2: R is reflexive by Def4;
A3: R is connected by A1, Def4;
let Y be set ; :: thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume that
A4: Y c= field R and
A5: Y <> {} ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
R is well_founded by A1, Def4;
then consider a being set such that
A6: a in Y and
A7: R -Seg a misses Y by A4, A5, Def2;
take a ; :: thesis: ( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
thus a in Y by A6; :: thesis: for b being set st b in Y holds
[a,b] in R
let b be set ; :: 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 A7, XBOOLE_0:3;
then ( a = b or not [b,a] in R ) by Def1;
then ( a <> b implies [a,b] in R ) by A3, A4, A6, A8, Lm4;
hence [a,b] in R by A2, A4, A6, Lm1; :: thesis: verum