let a, b be Real; for c being non zero Real holds |[a,b,c]| is non zero Element of (TOP-REAL 3)
let c be non zero Real; |[a,b,c]| is non zero Element of (TOP-REAL 3)
not |[a,b,c]| is zero
by EUCLID_5:4, FINSEQ_1:78;
hence
|[a,b,c]| is non zero Element of (TOP-REAL 3)
; verum