set X = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
let R1, R2 be Relation3 of ProjectivePoints V; ( ( 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 ) )
; 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 for u being object holds
( u in R1 iff u in R2 )let u be
object ;
( u in R1 iff u in R2 )A15:
now ( u in R2 implies u in R1 )assume A16:
u in R2
;
u in R1then 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;
verum end; now ( u in R1 implies u in R2 )assume A18:
u in R1
;
u in R2then 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;
verum end; hence
(
u in R1 iff
u in R2 )
by A15;
verum end;
hence
R1 = R2
by TARSKI:2; verum