let S be non empty with_nonpair_inputs ManySortedSign ; :: thesis: for x being Vertex of S st x is pair holds
x in InnerVertices S
let x be Vertex of S; :: thesis: ( x is pair implies x in InnerVertices S )
the carrier of S = (InputVertices S) \/ (InnerVertices S) by XBOOLE_1:45;
then ( x in InputVertices S or x in InnerVertices S ) by XBOOLE_0:def 3;
hence ( x is pair implies x in InnerVertices S ) by FACIRC_1:def 2; :: thesis: verum