let V be non trivial RealLinearSpace; :: thesis: for x, d, b, b9, d9, q being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

let x, d, b, b9, d9, q be Element of (ProjectiveSpace V); :: 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 (ProjectiveSpace V) 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 (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

A5: b9,q,b are_collinear by A3, Th24;

A6: b <> d by A1, Def7;

( b9,d9,o are_collinear & q,x,o are_collinear ) by A7; :: thesis: verum

ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

let x, d, b, b9, d9, q be Element of (ProjectiveSpace V); :: 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 (ProjectiveSpace V) 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 (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

A5: b9,q,b are_collinear by A3, Th24;

A6: b <> d by A1, Def7;

A7: now :: thesis: ( b <> b9 implies ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) )

( b9,d9,o are_collinear & q,x,o are_collinear ) )

A8:
b,b9,q are_collinear
by A3, Th24;

consider z being Element of (ProjectiveSpace V) such that

A9: b9,d9,z are_collinear and

A10: b,d,z are_collinear by A4, A5, Def9;

A11: z,b9,b9 are_collinear by Def7;

b,d,b are_collinear by Def7;

then z,b,x are_collinear by A2, A6, A10, Def8;

then consider o being Element of (ProjectiveSpace V) such that

A12: z,b9,o are_collinear and

A13: x,q,o are_collinear by A8, Def9;

A14: q,x,o are_collinear by A13, Th24;

assume A15: b <> b9 ; :: thesis: ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

A16: z <> b9

then b9,d9,o are_collinear by A12, A16, A11, Def8;

hence ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) by A14; :: thesis: verum

end;consider z being Element of (ProjectiveSpace V) such that

A9: b9,d9,z are_collinear and

A10: b,d,z are_collinear by A4, A5, Def9;

A11: z,b9,b9 are_collinear by Def7;

b,d,b are_collinear by Def7;

then z,b,x are_collinear by A2, A6, A10, Def8;

then consider o being Element of (ProjectiveSpace V) such that

A12: z,b9,o are_collinear and

A13: x,q,o are_collinear by A8, Def9;

A14: q,x,o are_collinear by A13, Th24;

assume A15: b <> b9 ; :: thesis: ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

A16: z <> b9

proof

z,b9,d9 are_collinear
by A9, Th24;
assume
not z <> b9
; :: thesis: contradiction

then A17: b,b9,d are_collinear by A10, Th24;

( b,b9,q are_collinear & b,b9,b are_collinear ) by A3, Def7, Th24;

hence contradiction by A1, A15, A17, Def8; :: thesis: verum

end;then A17: b,b9,d are_collinear by A10, Th24;

( b,b9,q are_collinear & b,b9,b are_collinear ) by A3, Def7, Th24;

hence contradiction by A1, A15, A17, Def8; :: thesis: verum

then b9,d9,o are_collinear by A12, A16, A11, Def8;

hence ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) by A14; :: thesis: verum

now :: thesis: ( b = b9 implies ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) )

hence
ex o being Element of (ProjectiveSpace V) st ( b9,d9,o are_collinear & q,x,o are_collinear ) )

assume
b = b9
; :: thesis: ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear )

then A18: d,b9,x are_collinear by A2, Th24;

d9,d,q are_collinear by A4, Th24;

then consider o being Element of (ProjectiveSpace V) such that

A19: d9,b9,o are_collinear and

A20: q,x,o are_collinear by A18, Def9;

b9,d9,o are_collinear by A19, Th24;

hence ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) by A20; :: thesis: verum

end;( b9,d9,o are_collinear & q,x,o are_collinear )

then A18: d,b9,x are_collinear by A2, Th24;

d9,d,q are_collinear by A4, Th24;

then consider o being Element of (ProjectiveSpace V) such that

A19: d9,b9,o are_collinear and

A20: q,x,o are_collinear by A18, Def9;

b9,d9,o are_collinear by A19, Th24;

hence ex o being Element of (ProjectiveSpace V) st

( b9,d9,o are_collinear & q,x,o are_collinear ) by A20; :: thesis: verum

( b9,d9,o are_collinear & q,x,o are_collinear ) by A7; :: thesis: verum