let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in InnerVertices S or ex b₁, b₂ being object st x = [b₁,b₂] )
consider A being MSAlgebra over S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
assume x in InnerVertices S ; :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being object 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;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum