theorem Th05: :: BKMODEL2:10

for a, b being Real
for c being non zero Real holds |[a,b,c]| is non zero Element of (TOP-REAL 3)