theorem Th3: :: FUNCT_6:3

for z being object
for X, Y being set holds ~ ([:X,Y:] --> z) = [:Y,X:] --> z