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