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