let FCPS be up-3-dimensional CollProjectiveSpace; for a, b, c, p, q, r being Element of FCPS st p <> q & p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,c,r are_coplanar
let a, b, c, p, q, r be Element of FCPS; ( p <> q & p,q,r are_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 are_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 are_collinear
by A2, Th1;
now ( not a,b,c are_collinear implies a,b,c,r are_coplanar )assume A6:
not
a,
b,
c are_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 ( not a,b,p are_collinear implies a,b,c,r are_coplanar )
b,
a,
b are_collinear
by ANPROJ_2:def 7;
then A9:
a,
b,
p,
b are_coplanar
by Th6;
a,
a,
b are_collinear
by ANPROJ_2:def 7;
then A10:
a,
b,
p,
a are_coplanar
by Th6;
assume A11:
not
a,
b,
p are_collinear
;
a,b,c,r are_coplanar
a,
b,
p,
c are_coplanar
by A3, Th7;
hence
a,
b,
c,
r are_coplanar
by A7, A11, A10, A9, Th8;
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 ( not a,b,q are_collinear implies a,b,c,r are_coplanar )
b,
a,
b are_collinear
by ANPROJ_2:def 7;
then A14:
a,
b,
q,
b are_coplanar
by Th6;
a,
a,
b are_collinear
by ANPROJ_2:def 7;
then A15:
a,
b,
q,
a are_coplanar
by Th6;
assume A16:
not
a,
b,
q are_collinear
;
a,b,c,r are_coplanar
a,
b,
q,
c are_coplanar
by A4, Th7;
hence
a,
b,
c,
r are_coplanar
by A12, A16, A15, A14, Th8;
verum end; now ( a,b,p are_collinear & a,b,q are_collinear implies a,b,c,r are_coplanar )assume
(
a,
b,
p are_collinear &
a,
b,
q are_collinear )
;
a,b,c,r are_coplanar then
a,
b,
r are_collinear
by A1, A2, COLLSP:9;
then
r,
a,
b are_collinear
by Th1;
hence
a,
b,
c,
r are_coplanar
by Th6;
verum end; hence
a,
b,
c,
r are_coplanar
by A8, A13;
verum end;
hence
a,b,c,r are_coplanar
by Th6; verum