let G1, G, G2 be Graph; :: thesis: ( G1 in bool G & G2 in bool G implies G1 \/ G2 in bool G )
assume that
A1: G1 in bool G and
A2: G2 in bool G ; :: thesis: G1 \/ G2 in bool G
A3: G1 is Subgraph of G by A1, Def25;
A4: G2 is Subgraph of G by A2, Def25;
A5: G1 c= G by A3, Def24;
A6: G2 c= G by A4, Def24;
A7: G1 \/ G2 c= G by A5, A6, Th22;
A8: G1 \/ G2 is Subgraph of G by A7, Def24;
thus G1 \/ G2 in bool G by A8, Def25; :: thesis: verum