let G1, G2 be strict Graph; :: thesis: ( G1 c= G2 implies ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) )
assume A1: G1 c= G2 ; :: thesis: ( G1 \/ G2 = G2 & G2 \/ G1 = G2 )
then ( G1 \/ G2 c= G2 & G2 c= G1 \/ G2 ) by Th20, Th22;
hence G1 \/ G2 = G2 by Th16; :: thesis: G2 \/ G1 = G2
hence G2 \/ G1 = G2 by A1, Th12; :: thesis: verum