consider x being object such that
A1: x in D by Def1;
x in D \/ X by A1, Def3;
hence ex x being object st x in D \/ X ; :: according to XBOOLE_0:def 1 :: thesis: verum