theorem Th20: :: GRAPH_1:20
for G1, G2 being Graph st ex G being Graph st
( G1 c= G & G2 c= G ) holds
( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )