theorem Th22: :: SYSREL:22

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