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