theorem Th2: :: FACIRC_1:2

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation