theorem :: YELLOW_2:21

for L being non empty RelStr holds id L is idempotent