theorem Th109: :: ZFMISC_1:110

for X1, X2, Y1, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 & Y1 = Y2 )