let F1, F2 be subset-closed set ; :: thesis: ( X c= F1 & ( for Y being set st X c= Y & Y is subset-closed holds
F1 c= Y ) & X c= F2 & ( for Y being set st X c= Y & Y is subset-closed holds
F2 c= Y ) implies F1 = F2 )
assume ( X c= F1 & ( for Y being set st X c= Y & Y is subset-closed holds
F1 c= Y ) & X c= F2 & ( for Y being set st X c= Y & Y is subset-closed holds
F2 c= Y ) ) ; :: thesis: F1 = F2
then ( F1 c= F2 & F2 c= F1 ) ;
hence F1 = F2 by XBOOLE_0:def 10; :: thesis: verum