let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & not InputVertices S1 is with_pair & not InputVertices S2 is with_pair implies not InputVertices (S1 +* S2) is with_pair )
assume S1 tolerates S2 ; :: thesis: ( InputVertices S1 is with_pair or InputVertices S2 is with_pair or not InputVertices (S1 +* S2) is with_pair )
then A1: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) by CIRCCOMB:11;
assume A2: for x being pair set holds not x in InputVertices S1 ; :: according to FACIRC_1:def 2 :: thesis: ( InputVertices S2 is with_pair or not InputVertices (S1 +* S2) is with_pair )
assume A3: for x being pair set holds not x in InputVertices S2 ; :: according to FACIRC_1:def 2 :: thesis: not InputVertices (S1 +* S2) is with_pair
let x be pair set ; :: 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