theorem Th20: :: FACIRC_1:20

for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds
( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )