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 set st
( a in Y & ( for b being set 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 set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume R well_orders X ; :: thesis: for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
then A1: ( R is_reflexive_in X & R is_connected_in X & R is_well_founded_in X ) by Def5;
let Y be set ; :: thesis: ( Y c= X & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume A2: ( Y c= X & Y <> {} ) ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
then consider a being set such that
A3: ( a in Y & R -Seg a misses Y ) by A1, Def3;
take a ; :: thesis: ( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
thus a in Y by A3; :: 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 A4: b in Y ; :: thesis: [a,b] in R
then not b in R -Seg a by A3, XBOOLE_0:3;
then ( a = b or not [b,a] in R ) by Def1;
then ( a <> b implies [a,b] in R ) by A1, A2, A3, A4, RELAT_2:def 6;
hence [a,b] in R by A1, A2, A3, RELAT_2:def 1; :: thesis: verum