let F be Field; :: thesis: for b, c, a, d being Element of (MPS F) st (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c
let b, c, a, d be Element of (MPS F); :: thesis: ( (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies a,b '||' a,c )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: b,c '||' a,d and
A3: a,b '||' c,d and
A4: a,c '||' b,d ; :: thesis: a,b '||' a,c
assume A5: not a,b '||' a,c ; :: thesis: contradiction
consider e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A6: ( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) ) by A3, Th2;
A7: ( a = e & b = f & c = g & d = h ) by A6, MCART_1:33;
then A8: [a,b,a,c] = [e,f,e,g] ;
A9: ( e = [(e `1 ),(e `2 ),(e `3 )] & f = [(f `1 ),(f `2 ),(f `3 )] & g = [(g `1 ),(g `2 ),(g `3 )] ) by MCART_1:48;
A10: ( h `1 = ((f `1 ) + (g `1 )) - (e `1 ) & h `2 = ((f `2 ) + (g `2 )) - (e `2 ) & h `3 = ((f `3 ) + (g `3 )) - (e `3 ) ) by A3, A4, A5, A6, Th5;
consider i, j, k, l being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A11: ( [b,c,a,d] = [i,j,k,l] & ( ex L being Element of F st
( L * ((i `1 ) - (j `1 )) = (k `1 ) - (l `1 ) & L * ((i `2 ) - (j `2 )) = (k `2 ) - (l `2 ) & L * ((i `3 ) - (j `3 )) = (k `3 ) - (l `3 ) ) or ( (i `1 ) - (j `1 ) = 0. F & (i `2 ) - (j `2 ) = 0. F & (i `3 ) - (j `3 ) = 0. F ) ) ) by A2, Th2;
A12: ( b = i & c = j & a = k & d = l ) by A11, MCART_1:33;
then ( i `1 <> j `1 or i `2 <> j `2 or i `3 <> j `3 ) by A5, A7, A8, A9, Th3;
then consider L being Element of F such that
A13: ( L * ((f `1 ) - (g `1 )) = (e `1 ) - (h `1 ) & L * ((f `2 ) - (g `2 )) = (e `2 ) - (h `2 ) & L * ((f `3 ) - (g `3 )) = (e `3 ) - (h `3 ) ) by A7, A11, A12, Lm2;
( (L - (1_ F)) * ((e `1 ) - (g `1 )) = (L + (1_ F)) * ((e `1 ) - (f `1 )) & (L - (1_ F)) * ((e `2 ) - (g `2 )) = (L + (1_ F)) * ((e `2 ) - (f `2 )) & (L - (1_ F)) * ((e `3 ) - (g `3 )) = (L + (1_ F)) * ((e `3 ) - (f `3 )) ) by A10, A13, Lm9;
then ( L + (1_ F) = 0. F & L - (1_ F) = 0. F ) by A5, A8, Th4;
then (L + (1_ F)) - (L - (1_ F)) = (0. F) + (- (0. F)) by RLVECT_1:def 12;
then (L + (1_ F)) - (L - (1_ F)) = 0. F by RLVECT_1:16;
then (L + (1_ F)) + (- (L - (1_ F))) = 0. F by RLVECT_1:def 12;
then (L + (1_ F)) + ((1_ F) + (- L)) = 0. F by RLVECT_1:47;
then ((L + (1_ F)) + (1_ F)) + (- L) = 0. F by RLVECT_1:def 6;
then (((1_ F) + (1_ F)) + L) + (- L) = 0. F by RLVECT_1:def 6;
then ((1_ F) + (1_ F)) + (L + (- L)) = 0. F by RLVECT_1:def 6;
then ((1_ F) + (1_ F)) + (0. F) = 0. F by RLVECT_1:16;
hence contradiction by A1, RLVECT_1:10; :: thesis: verum