let x1, x2, x3, x4, x5, x6, x7 be non pair set ; :: thesis: InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7}
set S1 = STC0IIStr (x1,x2,x3,x5,x6,x7);
{x4} misses InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) ;
then {x4} \ (InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7))) = {x4} by XBOOLE_1:83;
hence InputVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7)) = {x1,x2,x3,x4,x5,x6,x7} by ZFMISC_1:59, ThSTC0IS3; :: thesis: verum