defpred S1[ object ] means ex p, q, r being Element of V st
( \$1 = [(Dir p),(Dir q),(Dir r)] & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep );
set D = ProjectivePoints V;
set XXX = [:(),(),():];
consider R being set such that
A1: for xyz being object holds
( xyz in R iff ( xyz in [:(),(),():] & S1[xyz] ) ) from for x being object st x in R holds
x in [:(),(),():] by A1;
then R c= [:(),(),():] by TARSKI:def 3;
then reconsider R9 = R as Relation3 of ProjectivePoints V by COLLSP:def 1;
take R9 ; :: thesis: for x, y, z being object holds
( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )

let x, y, z be object ; :: thesis: ( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )

A2: now :: thesis: ( ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) implies [x,y,z] in R9 )
set xyz = [x,y,z];
given p, q, r being Element of V such that A3: ( x = Dir p & y = Dir q & z = Dir r ) and
A4: ( not p is zero & not q is zero ) and
A5: not r is zero and
A6: p,q,r are_LinDep ; :: thesis: [x,y,z] in R9
A7: Dir r is Element of ProjectivePoints V by ;
( Dir p is Element of ProjectivePoints V & Dir q is Element of ProjectivePoints V ) by ;
then [x,y,z] in [:(),(),():] by ;
hence [x,y,z] in R9 by A1, A3, A4, A5, A6; :: thesis: verum
end;
now :: thesis: ( [x,y,z] in R9 implies ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )
assume [x,y,z] in R9 ; :: thesis: ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep )

then consider p, q, r being Element of V such that
A8: [x,y,z] = [(Dir p),(Dir q),(Dir r)] and
A9: ( not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A1;
A10: z = Dir r by ;
( x = Dir p & y = Dir q ) by ;
hence ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by ; :: thesis: verum
end;
hence ( [x,y,z] in R9 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) by A2; :: thesis: verum