theorem Th155: :: ZF_LANG1:155

for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2