theorem Th25: :: CIRCTRM1:25

for S being non empty ManySortedSign holds S,S are_equivalent_wrt id the carrier of S, id the carrier' of S