theorem Th2: :: ANPROJ11:2
for a, b, c, d, e being Real holds |{|[a,1,0]|,|[b,0,1]|,|[c,d,e]|}| = (c - (a * d)) - (e * b)