let V be non trivial RealLinearSpace; :: thesis: for x, d, b, b9, d9, q being Element of () st not q,b,d are_collinear & b,d,x are_collinear & q,b9,b are_collinear & q,d9,d are_collinear holds
ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear )

let x, d, b, b9, d9, q be Element of (); :: thesis: ( not q,b,d are_collinear & b,d,x are_collinear & q,b9,b are_collinear & q,d9,d are_collinear implies ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear ) )

assume that
A1: not q,b,d are_collinear and
A2: b,d,x are_collinear and
A3: q,b9,b are_collinear and
A4: q,d9,d are_collinear ; :: thesis: ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear )

A5: b9,q,b are_collinear by ;
A6: b <> d by ;
A7: now :: thesis: ( b <> b9 implies ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear ) )
end;
now :: thesis: ( b = b9 implies ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear ) )
assume b = b9 ; :: thesis: ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear )

then A18: d,b9,x are_collinear by ;
d9,d,q are_collinear by ;
then consider o being Element of () such that
A19: d9,b9,o are_collinear and
A20: q,x,o are_collinear by ;
b9,d9,o are_collinear by ;
hence ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear ) by A20; :: thesis: verum
end;
hence ex o being Element of () st
( b9,d9,o are_collinear & q,x,o are_collinear ) by A7; :: thesis: verum