let G1, G2 be Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies (bool G1) \/ (bool G2) c= bool (G1 \/ G2) )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: (bool G1) \/ (bool G2) c= bool (G1 \/ G2)
A2: for v being set st v in bool G1 holds
v in bool (G1 \/ G2)

proof

let v be set ; :: thesis: ( v in bool G1 implies v in bool (G1 \/ G2) )
assume A3: v in bool G1 ; :: thesis: v in bool (G1 \/ G2)
reconsider G = v as strict Subgraph of G1 by A3, Def25;
A4: ( G c= G1 & G1 c= G1 \/ G2 ) by A1, Def24, Th19;
A5: G c= G1 \/ G2 by A4, Th17;
A6: G is strict Subgraph of G1 \/ G2 by A5, Def24;
thus v in bool (G1 \/ G2) by A6, Def25; :: thesis: verum

end;

A7: for v being set st v in bool G2 holds
v in bool (G1 \/ G2)

proof

let v be set ; :: thesis: ( v in bool G2 implies v in bool (G1 \/ G2) )
assume A8: v in bool G2 ; :: thesis: v in bool (G1 \/ G2)
reconsider G = v as strict Subgraph of G2 by A8, Def25;
A9: ( G c= G2 & G2 c= G1 \/ G2 ) by A1, Def24, Th19;
A10: G c= G1 \/ G2 by A9, Th17;
A11: G is strict Subgraph of G1 \/ G2 by A10, Def24;
thus v in bool (G1 \/ G2) by A11, Def25; :: thesis: verum

end;

A12: for v being set st v in (bool G1) \/ (bool G2) holds
v in bool (G1 \/ G2)

proof

let v be set ; :: thesis: ( v in (bool G1) \/ (bool G2) implies v in bool (G1 \/ G2) )
assume A13: v in (bool G1) \/ (bool G2) ; :: thesis: v in bool (G1 \/ G2)
A14: ( v in bool G1 or v in bool G2 ) by A13, XBOOLE_0:def 3;
thus v in bool (G1 \/ G2) by A2, A7, A14; :: thesis: verum

end;

thus (bool G1) \/ (bool G2) c= bool (G1 \/ G2) by A12, TARSKI:def 3; :: thesis: verum