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

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