let a, b be Real; :: thesis: for c being non zero Real holds |[a,b,c]| is non zero Element of (TOP-REAL 3)
let c be non zero Real; :: thesis: |[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) ; :: thesis: verum