theorem Th18: :: ANPROJ_8:21

for p, q, r being Point of (TOP-REAL 3)
for M being Matrix of 3,F_Real st M = <*p,q,r*> holds
( M * (1,1) = p `1 & M * (1,2) = p `2 & M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )