ex F being subset-closed set st
( F = union { (bool x) where x is Element of X : x in X } & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) ) by Lm1;
hence ex b₁ being subset-closed set st
( X c= b₁ & ( for Y being set st X c= Y & Y is subset-closed holds
b₁ c= Y ) ) ; :: thesis: verum