theorem Th13: :: WELLORD1:13

for X being set
for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X ) by Th12;