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