for R being non empty RelStr
for X being non empty Subset of R holds
( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )