let F be Field; :: thesis: for a, b, c being Element of (MPS F) holds a,b '||' c,c
let a, b, c be Element of (MPS F); :: thesis: a,b '||' c,c
consider e, f, g being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A1: [e,f,g,g] = [a,b,c,c] ;
A2: (((e `2 ) - (f `2 )) * ((g `3 ) - (g `3 ))) - (((g `2 ) - (g `2 )) * ((e `3 ) - (f `3 ))) = 0. F by Lm3;
( (((e `1 ) - (f `1 )) * ((g `2 ) - (g `2 ))) - (((g `1 ) - (g `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (g `3 ))) - (((g `1 ) - (g `1 )) * ((e `3 ) - (f `3 ))) = 0. F ) by Lm3;
hence a,b '||' c,c by A1, A2, Th23; :: thesis: verum