let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of X; :: thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete )
assume A1: ( A is open & B is open ) ; :: thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume A2: ( A is discrete & B is discrete ) ; :: thesis: A \/ B is discrete
for P, Q being Subset of X st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) by TOPS_1:37, TOPS_1:38;
hence A \/ B is discrete by A1, A2, Th30; :: thesis: verum