theorem :: SYSREL:17

for R being Relation st R c= id (dom R) holds
R = id (dom R)