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

A4: now

assume A5: b = b' ; :: thesis: ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear )
A6: d',d,q is_collinear by A1, Th25;
d,b',x is_collinear by A1, A5, Th25;
then consider o being Element of the carrier of (ProjectiveSpace V) such that
A7: ( d',b',o is_collinear & q,x,o is_collinear ) by A6, Def9;
( b',d',o is_collinear & q,x,o is_collinear ) by A7, Th25;
hence ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear ) ; :: thesis: verum

end;

now

assume A8: b <> b' ; :: thesis: ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear )
consider z being Element of (ProjectiveSpace V) such that
A9: ( b',d',z is_collinear & b,d,z is_collinear ) by A1, A3, Def9;
A10: z,b,x is_collinear

proof

b,d,b is_collinear by Def7;
hence z,b,x is_collinear by A1, A2, A9, Def8; :: thesis: verum

end;

b,b',q is_collinear by A1, Th25;
then consider o being Element of the carrier of (ProjectiveSpace V) such that
A11: ( z,b',o is_collinear & x,q,o is_collinear ) by A10, Def9;
A12: z <> b'

proof

assume not z <> b' ; :: thesis: contradiction
then A13: ( b,b',d is_collinear & b,b',q is_collinear ) by A1, A9, Th25;
b,b',b is_collinear by Def7;
hence contradiction by A1, A8, A13, Def8; :: thesis: verum

end;

A14: z,b',d' is_collinear by A9, Th25;
z,b',b' is_collinear by Def7;
then A15: b',d',o is_collinear by A11, A12, A14, Def8;
q,x,o is_collinear by A11, Th25;
hence ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear ) by A15; :: thesis: verum

end;

hence ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear ) by A4; :: thesis: verum