theorem Th12: :: PASCAL:12
for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) is symmetric