let x, y, c be set ; :: 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