let x be _Graph; :: according to GLIB_014:def 5 :: thesis: ( x in X \/ Y implies x is non-Dmulti )
assume x in X \/ Y ; :: thesis: x is non-Dmulti

per cases then ( x in X or x in Y ) by XBOOLE_0:def 3;

suppose x in X ; :: thesis: x is non-Dmulti

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

end;

suppose x in Y ; :: thesis: x is non-Dmulti

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

end;

end;