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:43;
A5: ( g `1 = 1_ F & g `2 = - (0. F) ) by A3, MCART_1:43;
the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] by PARSP_1:10;
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:43;
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 11
.= (((1. F) + (- (- (0. F)))) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:def 11
.= (((1. F) + (0. F)) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= (((1. F) + (0. F)) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= ((1. F) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - ((0. F) * ((1. F) - (1. F))) by RLVECT_1:15
.= ((1. F) * (1. F)) - (0. F) by VECTSP_1:12
.= (1. F) - (0. F) by VECTSP_1:def 8 ;

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:29;
( e9 = e & f9 = f ) by A6, A8, MCART_1:29;
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:12; :: thesis: verum