let V be non trivial RealLinearSpace; :: thesis: for x, d, b, b9, d9, q being Element of (ProjectiveSpace V) st not q,b,d is_collinear & b,d,x is_collinear & q,b9,b is_collinear & q,d9,d is_collinear holds
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear )
let x, d, b, b9, d9, q be Element of (ProjectiveSpace V); :: thesis: ( not q,b,d is_collinear & b,d,x is_collinear & q,b9,b is_collinear & q,d9,d is_collinear implies ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear ) )
assume that
A1: not q,b,d is_collinear and
A2: b,d,x is_collinear and
A3: q,b9,b is_collinear and
A4: q,d9,d is_collinear ; :: thesis: ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear )
A5: b9,q,b is_collinear by A3, Th25;
A6: b <> d by A1, Def7;

A7: now

A8: b,b9,q is_collinear by A3, Th25;
consider z being Element of (ProjectiveSpace V) such that
A9: b9,d9,z is_collinear and
A10: b,d,z is_collinear by A4, A5, Def9;
A11: z,b9,b9 is_collinear by Def7;
b,d,b is_collinear by Def7;
then z,b,x is_collinear by A2, A6, A10, Def8;
then consider o being Element of (ProjectiveSpace V) such that
A12: z,b9,o is_collinear and
A13: x,q,o is_collinear by A8, Def9;
A14: q,x,o is_collinear by A13, Th25;
assume A15: b <> b9 ; :: thesis: ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear )
A16: z <> b9

proof

assume not z <> b9 ; :: thesis: contradiction
then A17: b,b9,d is_collinear by A10, Th25;
( b,b9,q is_collinear & b,b9,b is_collinear ) by A3, Def7, Th25;
hence contradiction by A1, A15, A17, Def8; :: thesis: verum

end;

z,b9,d9 is_collinear by A9, Th25;
then b9,d9,o is_collinear by A12, A16, A11, Def8;
hence ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear ) by A14; :: thesis: verum

end;

now

assume b = b9 ; :: thesis: ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear )
then A18: d,b9,x is_collinear by A2, Th25;
d9,d,q is_collinear by A4, Th25;
then consider o being Element of (ProjectiveSpace V) such that
A19: d9,b9,o is_collinear and
A20: q,x,o is_collinear by A18, Def9;
b9,d9,o is_collinear by A19, Th25;
hence ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear ) by A20; :: thesis: verum

end;

hence ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear ) by A7; :: thesis: verum