let a, b be object ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being object 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 object 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 object st c in R -Seg a holds
( [c,b] in R & c <> b ) ; :: thesis: [a,b] in R
assume A3: not [a,b] in R ; :: thesis: contradiction
a <> b by A1, A3, Lm1;
then [b,a] in R by A1, A3, Lm4;
then b in R -Seg a by A3, Th1;
hence contradiction by A2; :: thesis: verum