let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & InputVertices S1 = InputVertices S2 implies InputVertices (S1 +* S2) = InputVertices S1 )
assume that
A1: S1 tolerates S2 and
A2: InputVertices S1 = InputVertices S2 ; :: thesis: InputVertices (S1 +* S2) = InputVertices S1
A3: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A4: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
thus InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) by A1, CIRCCMB2:5
.= (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) by A2, A4, XBOOLE_1:83
.= (InputVertices S1) \/ (InputVertices S2) by A2, A3, XBOOLE_1:83
.= InputVertices S1 by A2 ; :: thesis: verum