:: deftheorem Def8 defines PRs PARSP_1:def 9 :
for F being Field
for b₂ being set holds
( b₂ = PRs F iff for x being object holds
( x in b₂ iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) );