let p, q, r be Point of (TOP-REAL 3); :: thesis: for M being Matrix of 3,F_Real st M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> holds
( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r )
let M be Matrix of 3,F_Real; :: thesis: ( M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> implies ( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r ) )
assume A1: M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> ; :: thesis: ( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r )
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then ( Line (M,1) = M . 1 & Line (M,2) = M . 2 & Line (M,3) = M . 3 ) by MATRIX_0:52;
then ( Line (M,1) = <*(p `1),(p `2),(p `3)*> & Line (M,2) = <*(q `1),(q `2),(q `3)*> & Line (M,3) = <*(r `1),(r `2),(r `3)*> ) by A1, FINSEQ_1:45;
hence ( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r ) by EUCLID_5:3; :: thesis: verum