theorem Th3: :: EUCLID13:3

for r, s, t being Real st not r is zero & not s is zero & not t is zero holds
(((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1