let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & InputVertices S1 is without_pairs & InputVertices S2 is without_pairs implies InputVertices (S1 +* S2) is without_pairs )
assume S1 tolerates S2 ; :: thesis: ( not InputVertices S1 is without_pairs or not InputVertices S2 is without_pairs or InputVertices (S1 +* S2) is without_pairs )
then A1: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) by CIRCCOMB:11;
assume A2: for x being pair object holds not x in InputVertices S1 ; :: according to FACIRC_1:def 2 :: thesis: ( not InputVertices S2 is without_pairs or InputVertices (S1 +* S2) is without_pairs )
assume A3: for x being pair object holds not x in InputVertices S2 ; :: according to FACIRC_1:def 2 :: thesis: InputVertices (S1 +* S2) is without_pairs
let x be pair object ; :: according to FACIRC_1:def 2 :: thesis: not x in InputVertices (S1 +* S2)
assume x in InputVertices (S1 +* S2) ; :: thesis: contradiction
then ( x in InputVertices S1 or x in InputVertices S2 ) by A1, XBOOLE_0:def 3;
hence contradiction by A2, A3; :: thesis: verum