theorem Th29: :: WELLORD1:29

for a, b being object
for R being Relation st R is well-ordering & a in field R & b in field R holds
( [a,b] in R iff R -Seg a c= R -Seg b )