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