let U be set ; for A, B, C, D being Subset of U st Inter A,B <> {} & Inter A,B = Inter C,D holds
( A = C & B = D )
let A, B, C, D be Subset of U; ( Inter A,B <> {} & Inter A,B = Inter C,D implies ( A = C & B = D ) )
assume A0:
( Inter A,B <> {} & Inter A,B = Inter C,D )
; ( A = C & B = D )
then
A in Inter A,B
by KonceWInter;
then T1:
( C c= A & A c= D )
by Lemacik, A0;
C in Inter C,D
by A0, KonceWInter;
then t2:
( A c= C & C c= B )
by A0, Lemacik;
B in Inter A,B
by A0, KonceWInter;
then T4:
B c= D
by Lemacik, A0;
D in Inter C,D
by A0, KonceWInter;
then
D c= B
by A0, Lemacik;
hence
( A = C & B = D )
by t2, XBOOLE_0:def 10, T4, T1; verum