theorem Th154: :: ZF_LANG1:154

for x1, x2, y1, y2, z1, z2 being Variable holds
( (x1 'in' x2) / (y1,y2) = z1 'in' z2 iff ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )