theorem Th25: :: TEX_2:25

for Y being TopStruct st ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) holds
for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete