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