for G1, G2 being strict Graph st G1 c= G2 holds
( G1 \/ G2 = G2 & G2 \/ G1 = G2 )