set D = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
defpred S₁[ set ] 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 );
consider R being set such that
A1: for xyz being set holds
( xyz in R iff ( xyz in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] & S₁[xyz] ) ) from XBOOLE_0:sch 1();
R c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):]

proof

for x being set st x in R holds
x in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A1;
hence R c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by TARSKI:def 3; :: thesis: verum

end;

then reconsider R' = R as Relation3 of ProjectivePoints V by COLLSP:def 1;
take R' ; :: thesis: for x, y, z being set holds
( [x,y,z] in R' 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 set ; :: thesis: ( [x,y,z] in R' 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

assume [x,y,z] in R' ; :: 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
A3: ( [x,y,z] = [(Dir p),(Dir q),(Dir r)] & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A1;
( x = Dir p & y = Dir q & z = Dir r ) by A3, MCART_1:28;
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 A3; :: thesis: verum

end;

now

given p, q, r being Element of V such that A4: ( 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 ) ; :: thesis: [x,y,z] in R'
set xyz = [x,y,z];
( Dir p is Element of ProjectivePoints V & Dir q is Element of ProjectivePoints V & Dir r is Element of ProjectivePoints V ) by A4, Th34;
then [x,y,z] in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A4, MCART_1:73;
hence [x,y,z] in R' by A1, A4; :: thesis: verum

end;

hence ( [x,y,z] in R' 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