theorem Th14: :: NECKLA_3:14

for G being RelStr holds [: the carrier of G, the carrier of G:] = ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)