({} M) ` is closed ;
hence ex b₁ being Subset of M st
( b₁ is closed & not b₁ is empty ) ; :: thesis: verum