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