theorem Th14: :: WELLORD1:14

for a being object
for X being set
for R being Relation holds (R |_2 X) -Seg a c= R -Seg a