theorem Th27:
for
r125,
r136,
r246,
r345,
r126,
r135,
r245,
r346,
r157,
r259,
r597,
r368,
r268,
r297,
r247,
r287,
r358,
r587 being non
zero Real st
((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 &
r157 * r259 = - (r125 * r597) &
r126 * r368 = r136 * r268 &
r245 * r297 = - (r247 * r259) &
r247 * r268 = - (r246 * r287) &
r346 * r358 = r345 * r368 &
r135 * r587 = - (r157 * r358) holds
r287 * r597 = r297 * r587