let a, b be set ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) holds
[a,b] in R
let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) implies [a,b] in R )
assume that
A1: ( R is well-ordering & a in field R & b in field R ) and
A2: for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ; :: thesis: [a,b] in R
A3: R is connected by A1, Def4;
A4: R is reflexive by A1, Def4;
assume A5: not [a,b] in R ; :: thesis: contradiction
then a <> b by A1, A4, Lm1;
then [b,a] in R by A1, A3, A5, Lm4;
then b in R -Seg a by A5, Def1;
hence contradiction by A2; :: thesis: verum