theorem Th21: :: ANPROJ_8:24

for M being Matrix of 3,F_Real holds lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))}