:: deftheorem Def5 defines \/ GRAPH_1:def 5 :
for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
for b₃ being strict Graph holds
( b₃ = G1 \/ G2 iff ( the carrier of b₃ = the carrier of G1 \/ the carrier of G2 & the carrier' of b₃ = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b₃ . v = the Source of G1 . v & the Target of b₃ . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b₃ . v = the Source of G2 . v & the Target of b₃ . v = the Target of G2 . v ) ) ) );