theorem Th36: :: BKMODEL1:41

for a, b being Real holds not |[a,b,1]| is zero by EUCLID_5:4, FINSEQ_1:78;