consider A being MSAlgebra of S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
let x be set ; :: according to RELAT_1:def 1 :: thesis: ( not x in InnerVertices S or ex b<sub>1</sub>, b<sub>2</sub> being set st x = [b<sub>1</sub>,b<sub>2</sub>] )
assume x in InnerVertices S ; :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being set st x = [b<sub>1</sub>,b<sub>2</sub>]
then reconsider g = x as Gate of S by FACIRC_1:37;
g = [(g `1 ),(the Charact of A . g)] by A1, CIRCCOMB:def 10;
hence ex b₁, b₂ being set st x = [b₁,b₂] ; :: thesis: verum