let V be non trivial RealLinearSpace; :: thesis: for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
let p, p1, p2, r, r1 be Element of (ProjectiveSpace V); :: thesis: ( p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear implies ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
assume that
A1: p,p1,p2 are_collinear and
A2: p,p1,r are_collinear and
A3: p1,p2,r1 are_collinear ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
A4: now :: thesis: ( p <> p2 implies ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
A5: now :: thesis: ( p1 <> p implies ex r, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
assume A6: p1 <> p ; :: thesis: ex r, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
take r = r; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
A7: r,r1,r are_collinear by Def7;
p,p1,p are_collinear by Def7;
then p,p2,r are_collinear by A1, A2, A6, Def8;
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A7; :: thesis: verum
end;
A8: now :: thesis: ( p1 <> p2 implies ex r1, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
assume A9: p1 <> p2 ; :: thesis: ex r1, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
take r1 = r1; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
A10: r,r1,r1 are_collinear by Def7;
( p1,p2,p are_collinear & p1,p2,p2 are_collinear ) by A1, Def7, Th24;
then p,p2,r1 are_collinear by A3, A9, Def8;
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A10; :: thesis: verum
end;
assume p <> p2 ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A5, A8; :: thesis: verum
end;
now :: thesis: ( p = p2 implies ex r, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
assume p = p2 ; :: thesis: ex r, r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
then A11: p,p2,r are_collinear by Def7;
take r = r; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
r,r1,r are_collinear by Def7;
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A11; :: thesis: verum
end;
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A4; :: thesis: verum