defpred S1[ 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):] & S1[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 ) )
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 )
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;
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 ) )
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;
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 ) ) by A2; :: thesis: verum