theorem Th3:
for
r416,
r415,
r413,
r418,
r419,
r412,
r712,
r746,
r716,
r742,
r715,
r743,
r713,
r745,
r749,
r718,
r719,
r748 being non
zero Real st
(- r412) * (- r713) = (- r413) * (- r712) &
(- r415) * (- r719) = (- r419) * (- r715) &
(- r418) * (- r716) = (- r416) * (- r718) &
(- r745) * r416 = (- r746) * r415 &
(- r748) * r413 = (- r743) * r418 &
(- r742) * r419 = (- r749) * r412 &
r712 * r746 = r716 * r742 &
r715 * r743 = r713 * r745 holds
r718 * r749 = r719 * r748