let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & InnerVertices S1 is Relation & InnerVertices S2 is Relation implies InnerVertices (S1 +* S2) is Relation )
assume A1: S1 tolerates S2 ; :: thesis: ( not InnerVertices S1 is Relation or not InnerVertices S2 is Relation or InnerVertices (S1 +* S2) is Relation )
assume ( InnerVertices S1 is Relation & InnerVertices S2 is Relation ) ; :: thesis: InnerVertices (S1 +* S2) is Relation
then reconsider R1 = InnerVertices S1, R2 = InnerVertices S2 as Relation ;
R1 \/ R2 is Relation ;
hence InnerVertices (S1 +* S2) is Relation by A1, CIRCCOMB:11; :: thesis: verum