let p be FinSequence; :: thesis: for f being set holds [p,f] in InnerVertices (1GateCircStr p,f)
let f be set ; :: thesis: [p,f] in InnerVertices (1GateCircStr p,f)
InnerVertices (1GateCircStr p,f) = {[p,f]} by CIRCCOMB:49;
hence [p,f] in InnerVertices (1GateCircStr p,f) by TARSKI:def 1; :: thesis: verum