let f be set ; :: thesis: for p being FinSequence holds InnerVertices (1GateCircStr (p,f)) is Relation
let p be FinSequence; :: thesis: InnerVertices (1GateCircStr (p,f)) is Relation
InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;
hence InnerVertices (1GateCircStr (p,f)) is Relation ; :: thesis: verum