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