let F be Field; :: thesis: not for a, b, c being Element of (MPS F) 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 (MPS F) such that
A6: [a,b,a,c] = [e,f,e,g] ;
take a ; :: thesis: not for b, c being Element of (MPS F) holds a,b '||' a,c
take b ; :: thesis: not for c being Element of (MPS F) 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 14
.= (((1. F) + (- (- (0. F)))) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:def 14
.= (((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 e9, f9, g9, h9 be Element of [:the carrier of F,the carrier of F,the carrier of F:]; :: thesis: ( not [e9,f9,g9,h9] = [a,b,a,c] or (((e9 `1 ) - (f9 `1 )) * ((g9 `2 ) - (h9 `2 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `2 ) - (f9 `2 ))) <> 0. F or (((e9 `1 ) - (f9 `1 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F or (((e9 `2 ) - (f9 `2 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `2 ) - (h9 `2 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F )
assume A8: [e9,f9,g9,h9] = [a,b,a,c] ; :: thesis: ( (((e9 `1 ) - (f9 `1 )) * ((g9 `2 ) - (h9 `2 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `2 ) - (f9 `2 ))) <> 0. F or (((e9 `1 ) - (f9 `1 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F or (((e9 `2 ) - (f9 `2 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `2 ) - (h9 `2 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F )
then A9: ( g9 = e & h9 = g ) by A6, MCART_1:33;
( e9 = e & f9 = f ) by A6, A8, MCART_1:33;
hence ( (((e9 `1 ) - (f9 `1 )) * ((g9 `2 ) - (h9 `2 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `2 ) - (f9 `2 ))) <> 0. F or (((e9 `1 ) - (f9 `1 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `1 ) - (h9 `1 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F or (((e9 `2 ) - (f9 `2 )) * ((g9 `3 ) - (h9 `3 ))) - (((g9 `2 ) - (h9 `2 )) * ((e9 `3 ) - (f9 `3 ))) <> 0. F ) by A7, A9, Lm2; :: thesis: verum

end;

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