let F be Field; :: thesis: for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ( [a,b,c,d] in 4C3 F & 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] & (((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 ) ) )
let a, b, c, d be Element of (MPS F); :: thesis: ( a,b '||' c,d iff ( [a,b,c,d] in 4C3 F & 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] & (((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 ) ) )
( a,b '||' c,d iff [a,b,c,d] in PR F ) by Def6;
hence ( a,b '||' c,d iff ( [a,b,c,d] in 4C3 F & 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] & (((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 Def9; :: thesis: verum