let F be Field; :: thesis:
let a, b, p, q, r, s be Element of (MPS F); :: thesis:
defpred S₁[ Element of H₁(F), Element of H₁(F), Element of H₁(F), Element of H₁(F)] means ( ((($1 `1 ) - ($2 `1 )) * (($3 `2 ) - ($4 `2 ))) - ((($3 `1 ) - ($4 `1 )) * (($1 `2 ) - ($2 `2 ))) = 0. F & ((($1 `1 ) - ($2 `1 )) * (($3 `3 ) - ($4 `3 ))) - ((($3 `1 ) - ($4 `1 )) * (($1 `3 ) - ($2 `3 ))) = 0. F & ((($1 `2 ) - ($2 `2 )) * (($3 `3 ) - ($4 `3 ))) - ((($3 `2 ) - ($4 `2 )) * (($1 `3 ) - ($2 `3 ))) = 0. F );
assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s ; :: thesis:
consider e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A3: [e,f,g,h] = [a,b,p,q] and
A4: S₁[e,f,g,h] by A1, Th23;
consider i, j, k, l being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A5: [i,j,k,l] = [a,b,r,s] and
A6: S₁[i,j,k,l] by A2, Th23;
A7: ( i = a & j = b ) by A5, MCART_1:33;
A8: ( k = r & l = s ) by A5, MCART_1:33;
set A = (e `1 ) - (f `1 );
set B = (e `2 ) - (f `2 );
set C = (e `3 ) - (f `3 );
set D = (g `1 ) - (h `1 );
set E = (g `2 ) - (h `2 );
set K = (g `3 ) - (h `3 );
set G = (k `1 ) - (l `1 );
set H = (k `2 ) - (l `2 );
set I = (k `3 ) - (l `3 );
A9: ( e = a & f = b ) by A3, MCART_1:33;
A10: ( g = p & h = q ) by A3, MCART_1:33;

per cases ) - (f `1 ) <> 0. F or (e `2 ) - (f `2 ) <> 0. F or (e `3 ) - (f `3 ) <> 0. F ) by A12, RLVECT_1:35;

hence (((g `1 ) - (h `1 )) * ((k `2 ) - (l `2 ))) - (((k `1 ) - (l `1 )) * ((g `2 ) - (h `2 ))) = 0. F by A4, A6, A9, A7, Lm4; :: thesis:
thus A14: (((g `1 ) - (h `1 )) * ((k `3 ) - (l `3 ))) - (((k `1 ) - (l `1 )) * ((g `3 ) - (h `3 ))) = 0. F by A4, A6, A9, A7, A13, Lm4; :: thesis:
( ((g `2 ) - (h `2 )) * ((k `3 ) - (l `3 )) = ((((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) * (((e `1 ) - (f `1 )) " )) * ((k `3 ) - (l `3 )) & ((k `2 ) - (l `2 )) * ((g `3 ) - (h `3 )) = ((((k `1 ) - (l `1 )) * ((e `2 ) - (f `2 ))) * (((e `1 ) - (f `1 )) " )) * ((g `3 ) - (h `3 )) ) by A4, A6, A9, A7, A13, VECTSP_1:88;
hence (((g `2 ) - (h `2 )) * ((k `3 ) - (l `3 ))) - (((k `2 ) - (l `2 )) * ((g `3 ) - (h `3 ))) = 0. F by A14, Lm8; :: thesis:

end;

hence (((g `1 ) - (h `1 )) * ((k `2 ) - (l `2 ))) - (((k `1 ) - (l `1 )) * ((g `2 ) - (h `2 ))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis:
thus A16: (((g `2 ) - (h `2 )) * ((k `3 ) - (l `3 ))) - (((k `2 ) - (l `2 )) * ((g `3 ) - (h `3 ))) = 0. F by A4, A6, A9, A7, A15, Lm4; :: thesis:
( ((g `1 ) - (h `1 )) * ((k `3 ) - (l `3 )) = ((((g `2 ) - (h `2 )) * ((e `1 ) - (f `1 ))) * (((e `2 ) - (f `2 )) " )) * ((k `3 ) - (l `3 )) & ((k `1 ) - (l `1 )) * ((g `3 ) - (h `3 )) = ((((k `2 ) - (l `2 )) * ((e `1 ) - (f `1 ))) * (((e `2 ) - (f `2 )) " )) * ((g `3 ) - (h `3 )) ) by A4, A6, A9, A7, A15, VECTSP_1:88;
hence (((g `1 ) - (h `1 )) * ((k `3 ) - (l `3 ))) - (((k `1 ) - (l `1 )) * ((g `3 ) - (h `3 ))) = 0. F by A16, Lm8; :: thesis:

end;

hence (((g `2 ) - (h `2 )) * ((k `3 ) - (l `3 ))) - (((k `2 ) - (l `2 )) * ((g `3 ) - (h `3 ))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis:
A18: ( ((g `1 ) - (h `1 )) * ((k `2 ) - (l `2 )) = ((((g `3 ) - (h `3 )) * ((e `1 ) - (f `1 ))) * (((e `3 ) - (f `3 )) " )) * ((k `2 ) - (l `2 )) & ((k `1 ) - (l `1 )) * ((g `2 ) - (h `2 )) = ((((k `3 ) - (l `3 )) * ((e `1 ) - (f `1 ))) * (((e `3 ) - (f `3 )) " )) * ((g `2 ) - (h `2 )) ) by A4, A6, A9, A7, A17, VECTSP_1:88;
(((g `3 ) - (h `3 )) * ((k `2 ) - (l `2 ))) - (((k `3 ) - (l `3 )) * ((g `2 ) - (h `2 ))) = 0. F by A4, A6, A9, A7, A17, Lm6;
hence (((g `1 ) - (h `1 )) * ((k `2 ) - (l `2 ))) - (((k `1 ) - (l `1 )) * ((g `2 ) - (h `2 ))) = 0. F by A18, Lm8; :: thesis:
thus (((g `1 ) - (h `1 )) * ((k `3 ) - (l `3 ))) - (((k `1 ) - (l `1 )) * ((g `3 ) - (h `3 ))) = 0. F by A4, A6, A9, A7, A17, Lm6; :: thesis:

end;

hence ex g, h, k, l being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [g,h,k,l] = [p,q,r,s] & S₁[g,h,k,l] ) by A10, A8; :: thesis:

end;

hence ( p,q '||' r,s or a = b ) by Th23; :: thesis: