let x1, x2, x3, x5, x6, x7 be non pair set ; :: thesis: InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) is without_pairs
( InputVertices (BitGFA0Str (x1,x2,x3)) is without_pairs & InputVertices (BitGFA0Str (x5,x6,x7)) is without_pairs ) by GFACIRC1:35;
hence InputVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) is without_pairs by CIRCCOMB:47, FACIRC_1:8; :: thesis: verum