let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))
let M be Matrix of n,m,F_Real; :: thesis: lines M c= [#] (Lin (lines M))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lines M or x in [#] (Lin (lines M)) )
assume x in lines M ; :: thesis: x in [#] (Lin (lines M))
then x in Lin (lines M) by VECTSP_7:8;
hence x in [#] (Lin (lines M)) ; :: thesis: verum