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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F & (((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F ) and
A3: (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F by Th23;
A4: e = a by A1, MCART_1:33;
A5: g = a by A1, MCART_1:33;
then A6: (((f `2) - (e `2)) * ((f `3) - (h `3))) - (((f `2) - (h `2)) * ((f `3) - (e `3))) = 0. F by A3, A4, Lm13;
f = b by A1, MCART_1:33;
then A7: [f,e,f,h] = [b,a,b,c] by A1, A4, MCART_1:33;
( (((f `1) - (e `1)) * ((f `2) - (h `2))) - (((f `1) - (h `1)) * ((f `2) - (e `2))) = 0. F & (((f `1) - (e `1)) * ((f `3) - (h `3))) - (((f `1) - (h `1)) * ((f `3) - (e `3))) = 0. F ) by A2, A4, A5, Lm13;
hence b,a '||' b,c by A7, A6, Th23; :: thesis: verum