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;

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 )

hence
R1 = R2
by TARSKI:2; :: thesis: verum( u in R1 iff u in R2 )

let u be object ; :: thesis: ( u in R1 iff u in R2 )

end;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;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

now :: thesis: ( u in R1 implies u in R2 )

hence
( u in R1 iff u in R2 )
by A15; :: thesis: verumassume 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;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