let V be non trivial RealLinearSpace; :: thesis: for x, d, b, b', d', q being Element of 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 st
( b',d',o is_collinear & q,x,o is_collinear )
let x, d, b, b', d', q be Element of ; :: 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 st
( b',d',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,b',b is_collinear and
A4: q,d',d is_collinear ; :: thesis: ex o being Element of st
( b',d',o is_collinear & q,x,o is_collinear )
A5: b',q,b is_collinear by A3, Th25;
A6: b <> d by A1, Def7;

A7: now

A8: b,b',q is_collinear by A3, Th25;
consider z being Element of such that
A9: b',d',z is_collinear and
A10: b,d,z is_collinear by A4, A5, Def9;
A11: z,b',b' 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 such that
A12: z,b',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 <> b' ; :: thesis: ex o being Element of st
( b',d',o is_collinear & q,x,o is_collinear )
A16: z <> b'

proof

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

end;

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

end;

now

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

end;

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