( A1 is open & B1 is open ) by Th62;
then A1 /\ B1 is open by TOPS_1:38;
hence for b₁ being Subset of REAL st b₁ = A /\ B holds
b₁ is open by Th62; :: thesis: verum