let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for p, q, r, a, b, c being Element of FCPS st p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,c,r are_coplanar
let p, q, r, a, b, c be Element of FCPS; :: thesis: ( p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar implies a,b,c,r are_coplanar )
assume A1:
( p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar )
; :: thesis: a,b,c,r are_coplanar
then A2:
( a,b,q,c are_coplanar & q,p,r is_collinear )
by Th1, Th11;
now assume
not
a,
b,
c is_collinear
;
:: thesis: a,b,c,r are_coplanar then
(
a,
b,
p,
q are_coplanar &
a,
b,
q,
p are_coplanar )
by A1, Lm4;
then A3:
(
a,
b,
p,
r are_coplanar &
a,
b,
q,
r are_coplanar )
by A1, A2, Lm6;
A4:
now assume
(
a,
b,
p is_collinear &
a,
b,
q is_collinear )
;
:: thesis: a,b,c,r are_coplanar then
a,
b,
r is_collinear
by A1, COLLSP:14;
then
r,
a,
b is_collinear
by Th1;
hence
a,
b,
c,
r are_coplanar
by Th10;
:: thesis: verum end; A5:
now assume A6:
not
a,
b,
p is_collinear
;
:: thesis: a,b,c,r are_coplanar
(
a,
a,
b is_collinear &
b,
a,
b is_collinear )
by ANPROJ_2:def 7;
then
(
a,
b,
p,
a are_coplanar &
a,
b,
p,
b are_coplanar &
a,
b,
p,
c are_coplanar )
by A1, Th10, Th11;
hence
a,
b,
c,
r are_coplanar
by A3, A6, Th12;
:: thesis: verum end; now assume A7:
not
a,
b,
q is_collinear
;
:: thesis: a,b,c,r are_coplanar
(
a,
a,
b is_collinear &
b,
a,
b is_collinear )
by ANPROJ_2:def 7;
then
(
a,
b,
q,
a are_coplanar &
a,
b,
q,
b are_coplanar &
a,
b,
q,
c are_coplanar )
by A1, Th10, Th11;
hence
a,
b,
c,
r are_coplanar
by A3, A7, Th12;
:: thesis: verum end; hence
a,
b,
c,
r are_coplanar
by A4, A5;
:: thesis: verum end;
hence
a,b,c,r are_coplanar
by Th10; :: thesis: verum