for TS being TopSpace
for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds
P /\ Q is open_condensed