let F be Field; :: thesis: for a, p, b, c, q, r being Element of (MPS F) st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r
let a, p, b, c, q, r be Element of (MPS F); :: thesis: ( not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r )
assume that
A1: not a,p '||' a,b and
A2: not a,p '||' a,c and
A3: a,p '||' b,q and
A4: a,p '||' c,r and
A5: a,b '||' p,q and
A6: a,c '||' p,r ; :: thesis: b,c '||' q,r
consider i, j, k, l being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A7: [a,p,c,r] = [i,j,k,l] and
( 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 A4, Th2;
consider e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A8: [a,b,p,q] = [e,f,g,h] and
( 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 A5, Th2;
A9: ( a = e & p = g ) by A8, MCART_1:33;
A10: c = k by A7, MCART_1:33;
then A11: [a,p,c,r] = [e,g,k,l] by A9, A7, MCART_1:33;
then A12: l `1 = ((g `1 ) + (k `1 )) - (e `1 ) by A2, A4, A6, Th5;
A13: b = f by A8, MCART_1:33;
then A14: [a,p,b,q] = [e,g,f,h] by A8, A9, MCART_1:33;
then h `1 = ((g `1 ) + (f `1 )) - (e `1 ) by A1, A3, A5, Th5;
then A15: (1_ F) * ((f `1 ) - (k `1 )) = (h `1 ) - (l `1 ) by A12, Lm10;
A16: l `3 = ((g `3 ) + (k `3 )) - (e `3 ) by A2, A4, A6, A11, Th5;
A17: l `2 = ((g `2 ) + (k `2 )) - (e `2 ) by A2, A4, A6, A11, Th5;
h `3 = ((g `3 ) + (f `3 )) - (e `3 ) by A1, A3, A5, A14, Th5;
then A18: (1_ F) * ((f `3 ) - (k `3 )) = (h `3 ) - (l `3 ) by A16, Lm10;
h `2 = ((g `2 ) + (f `2 )) - (e `2 ) by A1, A3, A5, A14, Th5;
then A19: (1_ F) * ((f `2 ) - (k `2 )) = (h `2 ) - (l `2 ) by A17, Lm10;
q = h by A8, MCART_1:33;
then [b,c,q,r] = [f,k,h,l] by A13, A7, A10, MCART_1:33;
hence b,c '||' q,r by A15, A19, A18, Th2; :: thesis: verum