B = [#] (GX | B) by PRE_TOPC:def 5;
hence V /\ B is Subset of (GX | B) by XBOOLE_1:17; :: thesis: verum