for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B by Th23, SETFAM_1:def 9;