let S1, S2 be non empty ManySortedSign ; :: thesis: for v being Vertex of S1 holds
( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )
let v be Vertex of S1; :: thesis: ( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )
( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the carrier of (S2 +* S1) = the carrier of S2 \/ the carrier of S1 ) by CIRCCOMB:def 2;
hence ( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) ) by XBOOLE_0:def 3; :: thesis: verum