let S be ManySortedSign ; :: thesis: InducedEdges S c= [: the carrier' of S, the carrier of S:]

let x be object ; :: 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 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 ) ) by Def1;

hence x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def 2; :: thesis: verum

let x be object ; :: 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 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 ) ) by Def1;

hence x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def 2; :: thesis: verum