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_{1} being Subset of X st b_{1} = P \/ Q holds

b_{1} is open
by NORMSP_2:33; :: thesis: verum

( P1 is open & Q1 is open ) by NORMSP_2:33;

then P1 \/ Q1 is open ;

hence for b

b