let R1, R2 be Relation3 of ProjectivePoints V; :: thesis: ( ( for x, y, z being set 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 set 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
A5:
for x, y, z being set 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
A6:
for x, y, z being set 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
set X = ProjectivePoints V;
set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];
A7:
( R1 c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] & R2 c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] )
by COLLSP:def 1;
now let u be
set ;
:: thesis: ( u in R1 iff u in R2 )A8:
now assume A9:
u in R1
;
:: thesis: u in R2then consider x,
y,
z being
Element of
ProjectivePoints V such that A10:
u = [x,y,z]
by A7, DOMAIN_1:15;
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 A5, A9, A10;
hence
u in R2
by A6, A10;
:: thesis: verum end; now assume A11:
u in R2
;
:: thesis: u in R1then consider x,
y,
z being
Element of
ProjectivePoints V such that A12:
u = [x,y,z]
by A7, DOMAIN_1:15;
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 A6, A11, A12;
hence
u in R1
by A5, A12;
:: thesis: verum end; hence
(
u in R1 iff
u in R2 )
by A8;
:: thesis: verum end;
hence
R1 = R2
by TARSKI:2; :: thesis: verum