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