let D1, D2 be set ; :: thesis: ( D1 is PL-closed & ( for D being set st D is PL-closed holds
D1 c= D ) & D2 is PL-closed & ( for D being set st D is PL-closed holds
D2 c= D ) implies D1 = D2 )
assume that
A22: D1 is PL-closed and
A23: for D being set st D is PL-closed holds
D1 c= D and
A24: D2 is PL-closed and
A25: for D being set st D is PL-closed holds
D2 c= D ; :: thesis: D1 = D2
A26: D2 c= D1 by A22, A25;
D1 c= D2 by A23, A24;
hence D1 = D2 by A26, XBOOLE_0:def 10; :: thesis: verum