:: deftheorem defines symmetric_3 PASCAL:def 3 :
for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) = <*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*>;