theorem Th34: :: DIFF_1:34

for x0, x1, x2 being Real
for f being Function of REAL,REAL st x0,x1,x2 are_mutually_distinct holds
( [!f,x0,x1,x2!] = [!f,x1,x2,x0!] & [!f,x0,x1,x2!] = [!f,x2,x1,x0!] )