reconsider P1 = P, Q1 = Q as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

( P1 is closed & Q1 is closed ) by NORMSP_2:32;

then P1 /\ Q1 is closed ;

hence for b_{1} being Subset of X st b_{1} = P /\ Q holds

b_{1} is closed
by NORMSP_2:32; :: thesis: verum

( P1 is closed & Q1 is closed ) by NORMSP_2:32;

then P1 /\ Q1 is closed ;

hence for b

b