:: deftheorem Def1 defines InducedEdges MSSCYC_2:def 1 :
for S being ManySortedSign
for b₂ being set holds
( b₂ = InducedEdges S iff for x being object holds
( x in b₂ iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) );