let x, y, c be object ; 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; 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
; verum