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₂] )
assume A1: x in InnerVertices S ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
InnerVertices S = the carrier' of S by FACIRC_1:37;
then x = [( the Arity of S . x),(x `2)] by A1, CIRCCOMB:def 8;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum