theorem :: ANPROJ_8:26

for M being Matrix of 3,F_Real
for x being object holds
( x in lines (M @) iff ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) )