[#] M in Family_open_set M by PCOMPS_1:30;
then [#] M is open ;
hence ex b₁ being Subset of M st
( b₁ is open & not b₁ is empty ) ; :: thesis: verum