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:49;
hence InnerVertices (1GateCircStr p,f) is Relation ; :: thesis: verum