let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is open & Q is open holds
P \/ Q is open
let P, Q be Subset of TS; :: thesis: ( P is open & Q is open implies P \/ Q is open )
A1: (P ` ) /\ (Q ` ) = (P \/ Q) ` by XBOOLE_1:53;
assume ( P is open & Q is open ) ; :: thesis: P \/ Q is open
then ( P ` is closed & Q ` is closed ) ;
then (P \/ Q) ` is closed by A1, Th35;
hence P \/ Q is open by Th30; :: thesis: verum