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

( [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