theorem :: RELSET_2:42

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X