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:54;
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, Th36;
hence P /\ Q is open by Th30; :: thesis: verum