set X = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
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= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by COLLSP:def 1;
A14: R1 c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] 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 A13, DOMAIN_1:3;
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 A12, A16, A17;
hence u in R1 by A11, A17; :: 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 A14, DOMAIN_1:3;
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 A11, A18, A19;
hence u in R2 by A12, A19; :: thesis: verum

end;

hence ( u in R1 iff u in R2 ) by A15; :: thesis: verum

end;

hence R1 = R2 by TARSKI:2; :: thesis: verum