defpred S_{1}[ object ] means ex p, q, r being Element of V st

( $1 = [(Dir p),(Dir q),(Dir r)] & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep );

set D = ProjectivePoints V;

set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];

consider R being set such that

A1: for xyz being object holds

( xyz in R iff ( xyz in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] & S_{1}[xyz] ) )
from XBOOLE_0:sch 1();

for x being object st x in R holds

x in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A1;

then R c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by TARSKI:def 3;

then reconsider R9 = R as Relation3 of ProjectivePoints V by COLLSP:def 1;

take R9 ; :: thesis: for x, y, z being object holds

( [x,y,z] in R9 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 ) )

let x, y, z be object ; :: thesis: ( [x,y,z] in R9 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 ) )

( 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 A2; :: thesis: verum

( $1 = [(Dir p),(Dir q),(Dir r)] & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep );

set D = ProjectivePoints V;

set XXX = [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):];

consider R being set such that

A1: for xyz being object holds

( xyz in R iff ( xyz in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] & S

for x being object st x in R holds

x in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A1;

then R c= [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by TARSKI:def 3;

then reconsider R9 = R as Relation3 of ProjectivePoints V by COLLSP:def 1;

take R9 ; :: thesis: for x, y, z being object holds

( [x,y,z] in R9 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 ) )

let x, y, z be object ; :: thesis: ( [x,y,z] in R9 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 ) )

A2: now :: thesis: ( 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 [x,y,z] in R9 )

( 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 [x,y,z] in R9 )

set xyz = [x,y,z];

given p, q, r being Element of V such that A3: ( x = Dir p & y = Dir q & z = Dir r ) and

A4: ( not p is zero & not q is zero ) and

A5: not r is zero and

A6: p,q,r are_LinDep ; :: thesis: [x,y,z] in R9

A7: Dir r is Element of ProjectivePoints V by A5, Th21;

( Dir p is Element of ProjectivePoints V & Dir q is Element of ProjectivePoints V ) by A4, Th21;

then [x,y,z] in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A3, A7, MCART_1:69;

hence [x,y,z] in R9 by A1, A3, A4, A5, A6; :: thesis: verum

end;given p, q, r being Element of V such that A3: ( x = Dir p & y = Dir q & z = Dir r ) and

A4: ( not p is zero & not q is zero ) and

A5: not r is zero and

A6: p,q,r are_LinDep ; :: thesis: [x,y,z] in R9

A7: Dir r is Element of ProjectivePoints V by A5, Th21;

( Dir p is Element of ProjectivePoints V & Dir q is Element of ProjectivePoints V ) by A4, Th21;

then [x,y,z] in [:(ProjectivePoints V),(ProjectivePoints V),(ProjectivePoints V):] by A3, A7, MCART_1:69;

hence [x,y,z] in R9 by A1, A3, A4, A5, A6; :: thesis: verum

now :: thesis: ( [x,y,z] in R9 implies 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 ) )

hence
( [x,y,z] in R9 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 ) )

assume
[x,y,z] in R9
; :: thesis: 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 )

then consider p, q, r being Element of V such that

A8: [x,y,z] = [(Dir p),(Dir q),(Dir r)] and

A9: ( not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A1;

A10: z = Dir r by A8, XTUPLE_0:3;

( x = Dir p & y = Dir q ) by A8, XTUPLE_0:3;

hence 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 A9, A10; :: thesis: verum

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

then consider p, q, r being Element of V such that

A8: [x,y,z] = [(Dir p),(Dir q),(Dir r)] and

A9: ( not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by A1;

A10: z = Dir r by A8, XTUPLE_0:3;

( x = Dir p & y = Dir q ) by A8, XTUPLE_0:3;

hence 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 A9, A10; :: thesis: verum

( 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 A2; :: thesis: verum