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:42;

hence [p,f] in InnerVertices (1GateCircStr (p,f)) by TARSKI:def 1; :: thesis: verum

let f be set ; :: thesis: [p,f] in InnerVertices (1GateCircStr (p,f))

InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;

hence [p,f] in InnerVertices (1GateCircStr (p,f)) by TARSKI:def 1; :: thesis: verum