let G, G1, 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;
G2 c= G by A4;
then G1 \/ G2 c= G by A5, Th22;
then G1 \/ G2 is Subgraph of G ;
hence G1 \/ G2 in bool G by Def25; :: thesis: verum