for a, b, c, x, y, z being object holds
( ( b <> c implies ((a,b,c) --> (x,y,z)) . b = y ) & ((a,b,c) --> (x,y,z)) . c = z )