theorem Th38: :: SYSREL:38

for R, S being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} ) )