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