let S be ManySortedSign ; :: thesis: InducedEdges S c= [:the carrier' of S,the carrier of S:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in InducedEdges S or x in [:the carrier' of S,the carrier of S:] )
assume x in InducedEdges S ; :: thesis: x in [:the carrier' of S,the carrier of S:]
then consider op, v being set such that
A1: ( x = [op,v] & op in the carrier' of S & v in the carrier of S ) and
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 ) by Def1;
thus x in [:the carrier' of S,the carrier of S:] by A1, ZFMISC_1:def 2; :: thesis: verum