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 )
A2: ( G1 \/ G2 c= G2 & G2 c= G1 \/ G2 ) by A1, Th20, Th22;
thus A3: G1 \/ G2 = G2 by A2, Th16; :: thesis: G2 \/ G1 = G2
thus G2 \/ G1 = G2 by A1, A3, Th12; :: thesis: verum