theorem Th22: :: BKMODEL3:27

for a being non zero Real
for b, c being Real holds a * |[(b / a),(c / a),1]| = |[b,c,a]|