let x be _Graph; :: according to GLIB_014:def 5 :: thesis: ( x in {G1,G2} implies x is non-Dmulti )
assume x in {G1,G2} ; :: thesis: x is non-Dmulti

per cases then ( x = G1 or x = G2 ) by TARSKI:def 2;

suppose x = G1 ; :: thesis: x is non-Dmulti

hence x is non-Dmulti ; :: thesis: verum

end;

suppose x = G2 ; :: thesis: x is non-Dmulti

hence x is non-Dmulti ; :: thesis: verum

end;

end;