let F be Field; :: thesis: for a, b, c being Element of (MPS F) st a,b '||' a,c holds
b,a '||' b,c
let a, b, c be Element of (MPS F); :: thesis: ( a,b '||' a,c implies b,a '||' b,c )
assume a,b '||' a,c ; :: thesis: b,a '||' b,c
then consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [e,f,g,h] = [a,b,a,c] and
A2: ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F ) and
A3: (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by Th12;
A4: e = a by A1, XTUPLE_0:5;
A5: g = a by A1, XTUPLE_0:5;
then A6: (((f `2_3) - (e `2_3)) * ((f `3_3) - (h `3_3))) - (((f `2_3) - (h `2_3)) * ((f `3_3) - (e `3_3))) = 0. F by A3, A4, Lm13;
f = b by A1, XTUPLE_0:5;
then A7: [f,e,f,h] = [b,a,b,c] by A1, A4, XTUPLE_0:5;
( (((f `1_3) - (e `1_3)) * ((f `2_3) - (h `2_3))) - (((f `1_3) - (h `1_3)) * ((f `2_3) - (e `2_3))) = 0. F & (((f `1_3) - (e `1_3)) * ((f `3_3) - (h `3_3))) - (((f `1_3) - (h `1_3)) * ((f `3_3) - (e `3_3))) = 0. F ) by A2, A4, A5, Lm13;
hence b,a '||' b,c by A7, A6, Th12; :: thesis: verum