let p1, p2 be Element of REAL 3; :: thesis: ( p1,p2 are_ldependent2 implies p1 <X> p2 = 0.REAL 3 )
assume p1,p2 are_ldependent2 ; :: thesis: p1 <X> p2 = 0.REAL 3
then A1: ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & ( a1 <> 0 or a2 <> 0 ) ) by EUCLIDLP:def 2;

now :: thesis: ( ( ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a1 <> 0 ) & p1 <X> p2 = 0.REAL 3 ) or ( ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a2 <> 0 ) & p1 <X> p2 = 0.REAL 3 ) )

per cases ( ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a1 <> 0 ) or ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a2 <> 0 ) ) by A1;

case ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a1 <> 0 ) ; :: thesis: p1 <X> p2 = 0.REAL 3

then consider a1, a2 being Real such that
A2: ( a1 <> 0 & (a1 * p1) + (a2 * p2) = 0.REAL 3 ) ;
A3: (1 / a1) * (a1 * p1) = (1 / a1) * (- (a2 * p2)) by A2, RVSUM_1:23
.= (1 / a1) * (((- 1) * a2) * p2) by RVSUM_1:49
.= (1 / a1) * ((- a2) * p2) ;
A4: (1 / a1) * (a1 * p1) = (a1 * (1 / a1)) * p1 by EUCLID_4:4
.= 1 * p1 by A2, XCMPLX_1:106 ;
A5: 1 * p1 = |[(1 * (p1 . 1)),(1 * (p1 . 2)),(1 * (p1 . 3))]| by Lm1
.= p1 by Th1 ;
A6: 0.REAL 3 = |[0,0,0]| by FINSEQ_2:62;
p1 <X> p2 = (((- a2) * (1 / a1)) * p2) <X> p2 by A3, A4, A5, EUCLID_4:4
.= (((- a2) / a1) * p2) <X> p2 by XCMPLX_1:99 ;
then p1 <X> p2 = ((- a2) / a1) * (p2 <X> p2) by Lm14;
then p1 <X> p2 = ((- a2) / a1) * (0.REAL 3) by FINSEQ_2:62
.= |[(((- a2) / a1) * ((0.REAL 3) . 1)),(((- a2) / a1) * ((0.REAL 3) . 2)),(((- a2) / a1) * ((0.REAL 3) . 3))]| by Lm1
.= |[(((- a2) / a1) * 0),(((- a2) / a1) * ((0.REAL 3) . 2)),(((- a2) / a1) * ((0.REAL 3) . 3))]| by A6
.= |[0,(((- a2) / a1) * 0),(((- a2) / a1) * ((0.REAL 3) . 3))]| by A6
.= 0.REAL 3 by A6 ;
hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum

end;

case ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a2 <> 0 ) ; :: thesis: p1 <X> p2 = 0.REAL 3

then consider a1, a2 being Real such that
A7: ( a2 <> 0 & (a1 * p1) + (a2 * p2) = 0.REAL 3 ) ;
A8: (1 / a2) * (a2 * p2) = (1 / a2) * (- (a1 * p1)) by A7, RVSUM_1:23
.= (1 / a2) * (((- 1) * a1) * p1) by RVSUM_1:49
.= (1 / a2) * ((- a1) * p1) ;
A9: (1 / a2) * (a2 * p2) = (a2 * (1 / a2)) * p2 by EUCLID_4:4
.= 1 * p2 by A7, XCMPLX_1:106 ;
A10: 1 * p2 = |[(1 * (p2 . 1)),(1 * (p2 . 2)),(1 * (p2 . 3))]| by Lm1
.= p2 by Th1 ;
A11: 0.REAL 3 = |[0,0,0]| by FINSEQ_2:62;
p1 <X> p2 = p1 <X> (((- a1) * (1 / a2)) * p1) by A8, A9, A10, EUCLID_4:4
.= p1 <X> (((- a1) / a2) * p1) by XCMPLX_1:99
.= (((- a1) / a2) * p1) <X> p1 by Lm14
.= ((- a1) / a2) * (p1 <X> p1) by Lm14
.= ((- a1) / a2) * (0.REAL 3) by FINSEQ_2:62
.= |[(((- a1) / a2) * ((0.REAL 3) . 1)),(((- a1) / a2) * ((0.REAL 3) . 2)),(((- a1) / a2) * ((0.REAL 3) . 3))]| by Lm1
.= |[(((- a1) / a2) * 0),(((- a1) / a2) * ((0.REAL 3) . 2)),(((- a1) / a2) * ((0.REAL 3) . 3))]| by A11
.= |[0,(((- a1) / a2) * 0),(((- a1) / a2) * ((0.REAL 3) . 3))]| by A11
.= 0.REAL 3 by A11 ;
hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum

end;

end;

end;

hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum