let F be Field; :: thesis: for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b
let a, b, p, q, r, s be Element of (MPS F); :: thesis: ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b )
defpred S₁[ Element of H₁(F), Element of H₁(F), Element of H₁(F), Element of H₁(F)] means ( ((($1 `1_3) - ($2 `1_3)) * (($3 `2_3) - ($4 `2_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `2_3) - ($2 `2_3))) = 0. F & ((($1 `1_3) - ($2 `1_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F & ((($1 `2_3) - ($2 `2_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `2_3) - ($4 `2_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F );
assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s ; :: thesis: ( p,q '||' r,s or a = b )
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, Th12;
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, Th12;
A7: ( i = a & j = b ) by A5, XTUPLE_0:5;
A8: ( k = r & l = s ) by A5, XTUPLE_0:5;
set A = (e `1_3) - (f `1_3);
set B = (e `2_3) - (f `2_3);
set C = (e `3_3) - (f `3_3);
set D = (g `1_3) - (h `1_3);
set E = (g `2_3) - (h `2_3);
set K = (g `3_3) - (h `3_3);
set G = (k `1_3) - (l `1_3);
set H = (k `2_3) - (l `2_3);
set I = (k `3_3) - (l `3_3);
A9: ( e = a & f = b ) by A3, XTUPLE_0:5;
A10: ( g = p & h = q ) by A3, XTUPLE_0:5;

now :: thesis: ( a <> b implies 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] ) )

assume A11: a <> b ; :: thesis: 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] )

now :: thesis: ( ( (e `1_3) - (f `1_3) <> 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F ) or ( (e `2_3) - (f `2_3) <> 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F ) or ( (e `3_3) - (f `3_3) <> 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F ) )

e = [(e `1_3),(e `2_3),(e `3_3)] by MCART_1:44;
then A12: ( e `1_3 <> f `1_3 or e `2_3 <> f `2_3 or e `3_3 <> f `3_3 ) by A9, A11, MCART_1:44;

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

case A13: (e `1_3) - (f `1_3) <> 0. F ; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F )

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

end;

case A15: (e `2_3) - (f `2_3) <> 0. F ; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )

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

end;

case A17: (e `3_3) - (f `3_3) <> 0. F ; :: thesis: ( (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )

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

end;

end;

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: verum

end;

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