:: deftheorem defines +id YELLOW_9:def 2 :
for R being non empty RelStr
for X being non empty Subset of R holds X +id = (incl ((subrelstr X),R)) * ((subrelstr X) +id);