let U be set ; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: ( 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; :: thesis: verum