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:29;
A10: c = k by A7, MCART_1:29;
then A11: [a,p,c,r] = [e,g,k,l] by A9, A7, MCART_1:29;
then A12: l `1 = ((g `1) + (k `1)) - (e `1) by A2, A4, A6, Th5;
A13: b = f by A8, MCART_1:29;
then A14: [a,p,b,q] = [e,g,f,h] by A8, A9, MCART_1:29;
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:29;
then [b,c,q,r] = [f,k,h,l] by A13, A7, A10, MCART_1:29;
hence b,c '||' q,r by A15, A19, A18, Th2; :: thesis: verum