:: deftheorem defines .:^ RELSET_2:def 2 :
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds R .:^ X = Intersect ((.: R) .: {_{X}_});