:: deftheorem defines InducedGraph MSSCYC_2:def 4 :
for S being non empty ManySortedSign holds InducedGraph S = MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #);