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 A1: ( Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) ) ; :: thesis: ( A = C & B = D )

then A in Inter (A,B) by Th2;

then A2: ( C c= A & A c= D ) by Th1, A1;

C in Inter (C,D) by A1, Th2;

then A3: ( A c= C & C c= B ) by A1, Th1;

B in Inter (A,B) by A1, Th2;

then A4: B c= D by Th1, A1;

D in Inter (C,D) by A1, Th2;

then D c= B by A1, Th1;

hence ( A = C & B = D ) by A3, A4, A2; :: thesis: verum

( 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 A1: ( Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) ) ; :: thesis: ( A = C & B = D )

then A in Inter (A,B) by Th2;

then A2: ( C c= A & A c= D ) by Th1, A1;

C in Inter (C,D) by A1, Th2;

then A3: ( A c= C & C c= B ) by A1, Th1;

B in Inter (A,B) by A1, Th2;

then A4: B c= D by Th1, A1;

D in Inter (C,D) by A1, Th2;

then D c= B by A1, Th1;

hence ( A = C & B = D ) by A3, A4, A2; :: thesis: verum