let F be Field; :: thesis: for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) )
let a, b, c, d be Element of (MPS F); :: thesis: ( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) )
A1: ( a,b '||' c,d implies ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) )

proof

assume a,b '||' c,d ; :: thesis: ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) )
then consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A2: [a,b,c,d] = [e,f,g,h] and
A3: ( (((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 & (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) by PARSP_1:12;
( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) by A3, Lm3;
hence ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) by A2; :: thesis: verum

end;

( ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) implies a,b '||' c,d )

proof

given e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that A4: [a,b,c,d] = [e,f,g,h] and
A5: ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ; :: thesis: a,b '||' c,d
A6: (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F by A5, Lm3;
( (((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 ) by A5, Lm3;
hence a,b '||' c,d by A4, A6, PARSP_1:12; :: thesis: verum

end;

hence ( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) ) ) by A1; :: thesis: verum