theorem Th46: :: RELSET_2:46

for A, B being set
for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))