# Tetradron Theorem
Tetradron := Theorem(
    [y2^2+y3^2-y1^2, (y2-y1)^2+y3^2-y1^2, y4^2+y5^2+y6^2-y1^2,
     (y4-y1)^2+y5^2+y6^2-y1^2, (y5-y2)^2+(y5-y3)^2+y6^2-y1^2,
     2*y7-y1, 2*y8-y1-y2, 2*y9-y3, 2*y10-y2, 2*y11-y3,
     2*y12-y4-y2, 2*y13-y5-y3,2*y14-y6, 2*y15-y4,
     2*y16-y5, 2*y17-y6, 2*y18-y4-y1, 2*y19-y5, 2*y20-y6,
     (y21-y7)*y13-y22*(y12-y7), y22*y14-y23*y13, (y21-y8)*y17-y23*(y15-y8)],
    [(y22-y9)*y17-y23*(y16-y8),(y21-y10)*y20-y23*(y18-y10),
     (y22-y11)*y20-y23*(y19-y11),
     (y21-y7)^2+y22^2+y23^2-(y21-y12)^2-(y22-y13)^2-(y23-y14)^2,
     (y12-y7)*(y15-y8)+y13*(y16-y9)+y14*y17],
    [y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15, y16, y17, 
     y18, y19, y20, y21, y22, y23]);
