theorem Th1: :: MSSCYC_2:1

for S being ManySortedSign holds InducedEdges S c= [: the carrier' of S, the carrier of S:]