theorem Th3: :: YELLOW_6:3

for R being RelStr holds the carrier of R = the carrier of (R ~)