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