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, MCART_1:93;
A5: g = a by A1, MCART_1:93;
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, MCART_1:93;
then A7: [[f,e],[f,h]] = [[b,a],[b,c]] by A1, A4, MCART_1:93;
( (((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