for G, G1, G2 being Graph st G1 in bool G & G2 in bool G holds
G1 \/ G2 in bool G