theorem Th31: :: RELSET_2:31

for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1