theorem Th35: :: WELLORD1:35

for R being Relation
for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being object st a in field R holds
[a,(F . a)] in R