theorem Th9: :: WELLORD1:9

for a being object
for R being Relation holds R -Seg a c= field R