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