let FCPS be up-3-dimensional CollProjectiveSpace; 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; ( 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 that
A1:
p <> q
and
A2:
p,q,r is_collinear
and
A3:
a,b,c,p are_coplanar
and
A4:
a,b,c,q are_coplanar
; a,b,c,r are_coplanar
A5:
q,p,r is_collinear
by A2, Th1;
now assume A6:
not
a,
b,
c is_collinear
;
a,b,c,r are_coplanar then
a,
b,
p,
q are_coplanar
by A3, A4, Lm4;
then A7:
a,
b,
p,
r are_coplanar
by A1, A2, Lm6;
A8:
now
b,
a,
b is_collinear
by ANPROJ_2:def 7;
then A9:
a,
b,
p,
b are_coplanar
by Th10;
a,
a,
b is_collinear
by ANPROJ_2:def 7;
then A10:
a,
b,
p,
a are_coplanar
by Th10;
assume A11:
not
a,
b,
p is_collinear
;
a,b,c,r are_coplanar
a,
b,
p,
c are_coplanar
by A3, Th11;
hence
a,
b,
c,
r are_coplanar
by A7, A11, A10, A9, Th12;
verum end;
a,
b,
q,
p are_coplanar
by A3, A4, A6, Lm4;
then A12:
a,
b,
q,
r are_coplanar
by A1, A5, Lm6;
A13:
now
b,
a,
b is_collinear
by ANPROJ_2:def 7;
then A14:
a,
b,
q,
b are_coplanar
by Th10;
a,
a,
b is_collinear
by ANPROJ_2:def 7;
then A15:
a,
b,
q,
a are_coplanar
by Th10;
assume A16:
not
a,
b,
q is_collinear
;
a,b,c,r are_coplanar
a,
b,
q,
c are_coplanar
by A4, Th11;
hence
a,
b,
c,
r are_coplanar
by A12, A16, A15, A14, Th12;
verum end; now assume
(
a,
b,
p is_collinear &
a,
b,
q is_collinear )
;
a,b,c,r are_coplanar then
a,
b,
r is_collinear
by A1, A2, COLLSP:9;
then
r,
a,
b is_collinear
by Th1;
hence
a,
b,
c,
r are_coplanar
by Th10;
verum end; hence
a,
b,
c,
r are_coplanar
by A8, A13;
verum end;
hence
a,b,c,r are_coplanar
by Th10; verum