let D1, D2 be non empty set ; :: thesis: ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D2 c= D ) implies D1 = D2 )
assume ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D2 c= D ) ) ; :: thesis: D1 = D2
then ( D1 c= D2 & D2 c= D1 ) ;
hence D1 = D2 by XBOOLE_0:def 10; :: thesis: verum