theorem Th21: :: YELLOW_3:21

for S1, S2 being non empty RelStr
for D being non empty Subset of [:S1,S2:] holds
( not proj1 D is empty & not proj2 D is empty )