let R be POINT of (IncProjSp_of real_projective_plane); :: thesis: for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let p, q be Point of real_projective_plane; :: thesis: for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) implies ( R on L iff |{u,v,w}| = 0 ) )
assume that
A1: p = Dir u and
A2: q = Dir v and
A3: R = Dir w and
A4: L = Line (p,q) ; :: thesis: ( R on L iff |{u,v,w}| = 0 )
reconsider r = Dir w as Point of real_projective_plane by ANPROJ_1:26;

hereby :: thesis: ( |{u,v,w}| = 0 implies R on L )

assume R on L ; :: thesis: |{u,v,w}| = 0
then p,q,r are_collinear by A3, A4, Th61;
then consider u1, v1, w1 being Element of (TOP-REAL 3) such that
A5: p = Dir u1 and
A6: q = Dir v1 and
A7: r = Dir w1 and
A8: ( not u1 is zero & not v1 is zero & not w1 is zero ) and
A9: ( u1 = v1 or u1 = w1 or v1 = w1 or {u1,v1,w1} is linearly-dependent ) by ANPROJ_8:10;
u1,v1,w1 are_LinDep by A9, ANPROJ_8:9;
then |{u1,v1,w1}| = 0 by ANPROJ_8:43;
then |{u,v1,w1}| = 0 by A1, A5, A8, ANPROJ_8:58;
then |{u,v,w1}| = 0 by A2, A6, A8, ANPROJ_8:59;
hence |{u,v,w}| = 0 by A8, A7, ANPROJ_8:60; :: thesis: verum

end;

assume |{u,v,w}| = 0 ; :: thesis: R on L
then ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) by ANPROJ_8:9, ANPROJ_8:43;
then p,q,r are_collinear by A1, A2, ANPROJ_8:10;
hence R on L by A3, A4, Th61; :: thesis: verum