let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of X; :: thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A1: A is closed and
A2: B is closed ; :: thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A3: A is discrete and
A4: B is discrete ; :: thesis: A \/ B is discrete
for P, Q being Subset of X st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ;
hence A \/ B is discrete by A1, A2, A3, A4, Th25; :: thesis: verum