theorem :: YELLOW12:22

for R being non empty reflexive RelStr holds id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~)