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_3) - (f `2_3)) * ((g `3_3) - (g `3_3))) - (((g `2_3) - (g `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by Lm3;
( (((e `1_3) - (f `1_3)) * ((g `2_3) - (g `2_3))) - (((g `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (g `3_3))) - (((g `1_3) - (g `1_3)) * ((e `3_3) - (f `3_3))) = 0. F ) by Lm3;
hence a,b '||' c,c by A1, A2, Th12; :: thesis: verum