theorem Th6: :: ZFMODEL2:6

for x, y, z being Variable
for M being non empty set
for m1, m2, m3 being Element of M
for v being Function of VAR,M st x <> y & y <> z & z <> x holds
( ((v / (x,m1)) / (y,m2)) / (z,m3) = ((v / (z,m3)) / (y,m2)) / (x,m1) & ((v / (x,m1)) / (y,m2)) / (z,m3) = ((v / (y,m2)) / (z,m3)) / (x,m1) )