let F be Field; :: thesis: not for a, b, c being Element of holds a,b '||' a,c
consider e, f, g being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A1: e = [(1_ F),(1_ F),(0. F)] and
A2: f = [(- (0. F)),(1_ F),(0. F)] and
A3: g = [(1_ F),(- (0. F)),(0. F)] ;
A4: ( f `1 = - (0. F) & f `2 = 1_ F ) by A2, MCART_1:47;
A5: ( g `1 = 1_ F & g `2 = - (0. F) ) by A3, MCART_1:47;
the carrier of (MPS F) = [:the carrier of F,the carrier of F,the carrier of F:] by PARSP_1:21;
then consider a, b, c being Element of such that
A6: [a,b,a,c] = [e,f,e,g] ;
take a ; :: thesis: not for b, c being Element of holds a,b '||' a,c
take b ; :: thesis: not for c being Element of holds a,b '||' a,c
take c ; :: thesis: not a,b '||' a,c
( e `1 = 1_ F & e `2 = 1_ F ) by A1, MCART_1:47;
then A7: (((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 ))) - (((e `1 ) - (g `1 )) * ((e `2 ) - (f `2 ))) = (((1. F) + (- (- (0. F)))) * ((1. F) - (- (0. F)))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by A4, A5, RLVECT_1:def 12
.= (((1. F) + (- (- (0. F)))) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:def 12
.= (((1. F) + (0. F)) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:30
.= (((1. F) + (0. F)) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:30
.= ((1. F) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:10
.= ((1. F) * (1. F)) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:10
.= ((1. F) * (1. F)) - ((0. F) * ((1. F) - (1. F))) by RLVECT_1:28
.= ((1. F) * (1. F)) - (0. F) by VECTSP_1:44
.= (1. F) - (0. F) by VECTSP_1:def 19 ;

now

let e', f', g', h' be Element of [:the carrier of F,the carrier of F,the carrier of F:]; :: thesis: ( not [e',f',g',h'] = [a,b,a,c] or (((e' `1 ) - (f' `1 )) * ((g' `2 ) - (h' `2 ))) - (((g' `1 ) - (h' `1 )) * ((e' `2 ) - (f' `2 ))) <> 0. F or (((e' `1 ) - (f' `1 )) * ((g' `3 ) - (h' `3 ))) - (((g' `1 ) - (h' `1 )) * ((e' `3 ) - (f' `3 ))) <> 0. F or (((e' `2 ) - (f' `2 )) * ((g' `3 ) - (h' `3 ))) - (((g' `2 ) - (h' `2 )) * ((e' `3 ) - (f' `3 ))) <> 0. F )
assume A8: [e',f',g',h'] = [a,b,a,c] ; :: thesis: ( (((e' `1 ) - (f' `1 )) * ((g' `2 ) - (h' `2 ))) - (((g' `1 ) - (h' `1 )) * ((e' `2 ) - (f' `2 ))) <> 0. F or (((e' `1 ) - (f' `1 )) * ((g' `3 ) - (h' `3 ))) - (((g' `1 ) - (h' `1 )) * ((e' `3 ) - (f' `3 ))) <> 0. F or (((e' `2 ) - (f' `2 )) * ((g' `3 ) - (h' `3 ))) - (((g' `2 ) - (h' `2 )) * ((e' `3 ) - (f' `3 ))) <> 0. F )
then A9: ( g' = e & h' = g ) by A6, MCART_1:33;
( e' = e & f' = f ) by A6, A8, MCART_1:33;
hence ( (((e' `1 ) - (f' `1 )) * ((g' `2 ) - (h' `2 ))) - (((g' `1 ) - (h' `1 )) * ((e' `2 ) - (f' `2 ))) <> 0. F or (((e' `1 ) - (f' `1 )) * ((g' `3 ) - (h' `3 ))) - (((g' `1 ) - (h' `1 )) * ((e' `3 ) - (f' `3 ))) <> 0. F or (((e' `2 ) - (f' `2 )) * ((g' `3 ) - (h' `3 ))) - (((g' `2 ) - (h' `2 )) * ((e' `3 ) - (f' `3 ))) <> 0. F ) by A7, A9, Lm2; :: thesis: verum

end;

hence not a,b '||' a,c by PARSP_1:23; :: thesis: verum