reconsider P1 = P, Q1 = Q as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
( P1 is open & Q1 is open ) by NORMSP_2:33;
then P1 /\ Q1 is open ;
hence for b₁ being Subset of X st b₁ = P /\ Q holds
b₁ is open by NORMSP_2:33; :: thesis: verum