theorem Th15: :: PASCAL:15

for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being Real st symmetric_3 (a1,a2,a3,a4,a5,a6) = symmetric_3 (b1,b2,b3,b4,b5,b6) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 )