theorem Th34: :: WELLORD1:34

for a, b being object
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