set X = ProjectivePoints V;
set XXX = [:(),(),():];
let R1, R2 be Relation3 of ProjectivePoints V; :: thesis: ( ( for x, y, z being object holds
( [x,y,z] in R1 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 ) ) ) & ( for x, y, z being object holds
( [x,y,z] in R2 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 ) ) ) implies R1 = R2 )

assume that
A11: for x, y, z being object holds
( [x,y,z] in R1 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 ) ) and
A12: for x, y, z being object holds
( [x,y,z] in R2 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 ) ) ; :: thesis: R1 = R2
A13: R2 c= [:(),(),():] by COLLSP:def 1;
A14: R1 c= [:(),(),():] by COLLSP:def 1;
now :: thesis: for u being object holds
( u in R1 iff u in R2 )
let u be object ; :: thesis: ( u in R1 iff u in R2 )
A15: now :: thesis: ( u in R2 implies u in R1 )
assume A16: u in R2 ; :: thesis: u in R1
then consider x, y, z being Element of ProjectivePoints V such that
A17: u = [x,y,z] by ;
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 ;
hence u in R1 by ; :: thesis: verum
end;
now :: thesis: ( u in R1 implies u in R2 )
assume A18: u in R1 ; :: thesis: u in R2
then consider x, y, z being Element of ProjectivePoints V such that
A19: u = [x,y,z] by ;
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 ;
hence u in R2 by ; :: thesis: verum
end;
hence ( u in R1 iff u in R2 ) by A15; :: thesis: verum
end;
hence R1 = R2 by TARSKI:2; :: thesis: verum