theorem Th9: :: PARSP_1:9

for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ( [[a,b],[c,d]] in 4C_3 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_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) ) by Def8;