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

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