let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: InnerVertices (2GatesCircStr (x,y,c,f)) is Relation

InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;

hence InnerVertices (2GatesCircStr (x,y,c,f)) is Relation ; :: thesis: verum

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: InnerVertices (2GatesCircStr (x,y,c,f)) is Relation

InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;

hence InnerVertices (2GatesCircStr (x,y,c,f)) is Relation ; :: thesis: verum