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;
A7: now :: thesis: ( b <> b9 implies ex o being Element of (ProjectiveSpace V) st
( 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
proof
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;
z,b9,d9 are_collinear by A9, Th24;
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;
now :: thesis: ( b = b9 implies 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;
hence ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear ) by A7; :: thesis: verum