theorem Th27: :: WAYBEL19:27

for R being non empty RelStr
for X being non empty Subset of R holds
( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )