let E1, E2 be set ; :: thesis: ( E1 is MC-closed & ( for E being set st E is MC-closed holds
E1 c= E ) & E2 is MC-closed & ( for E being set st E is MC-closed holds
E2 c= E ) implies E1 = E2 )
assume that
A33: E1 is MC-closed and
A34: for E being set st E is MC-closed holds
E1 c= E and
A35: E2 is MC-closed and
A36: for E being set st E is MC-closed holds
E2 c= E ; :: thesis: E1 = E2
A37: E2 c= E1 by A33, A36;
E1 c= E2 by A34, A35;
hence E1 = E2 by A37, XBOOLE_0:def 10; :: thesis: verum