S1 tolerates S2 by CIRCCOMB:47;
then InputVertices (S1 +* S2) is Subset of ((InputVertices S1) \/ (InputVertices S2)) by CIRCCOMB:11;
hence InputVertices (S1 +* S2) is without_pairs ; :: according to CIRCCMB3:def 11 :: thesis: verum