let FCPS be up-3-dimensional CollProjectiveSpace; for a, b, c, p, q, r being Element of FCPS st not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar holds
a,p,q,r are_coplanar
let a, b, c, p, q, r be Element of FCPS; ( not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar implies a,p,q,r are_coplanar )
assume that
A1:
not a,b,c are_collinear
and
A2:
a,b,c,p are_coplanar
and
A3:
a,b,c,q are_coplanar
and
A4:
a,b,c,r are_coplanar
; a,p,q,r are_coplanar
now ( not p,q,r are_collinear implies a,p,q,r are_coplanar )A5:
now ( not a,r,b are_collinear implies a,p,q,r are_coplanar )
a,
b,
r,
q are_coplanar
by A1, A3, A4, Lm4;
then A6:
a,
r,
b,
q are_coplanar
by Th7;
a,
b,
r,
p are_coplanar
by A1, A2, A4, Lm4;
then A7:
a,
r,
b,
p are_coplanar
by Th7;
assume
not
a,
r,
b are_collinear
;
a,p,q,r are_coplanar then
a,
r,
p,
q are_coplanar
by A7, A6, Lm4;
hence
a,
p,
q,
r are_coplanar
by Th7;
verum end; A8:
now ( not a,p,b are_collinear implies a,p,q,r are_coplanar )
a,
b,
p,
r are_coplanar
by A1, A2, A4, Lm4;
then A9:
a,
p,
b,
r are_coplanar
by Th7;
a,
b,
p,
q are_coplanar
by A1, A2, A3, Lm4;
then A10:
a,
p,
b,
q are_coplanar
by Th7;
assume
not
a,
p,
b are_collinear
;
a,p,q,r are_coplanar hence
a,
p,
q,
r are_coplanar
by A10, A9, Lm4;
verum end; A11:
now ( not a,q,b are_collinear implies a,p,q,r are_coplanar )
a,
b,
q,
r are_coplanar
by A1, A3, A4, Lm4;
then A12:
a,
q,
b,
r are_coplanar
by Th7;
a,
b,
q,
p are_coplanar
by A1, A2, A3, Lm4;
then A13:
a,
q,
b,
p are_coplanar
by Th7;
assume
not
a,
q,
b are_collinear
;
a,p,q,r are_coplanar then
a,
q,
p,
r are_coplanar
by A13, A12, Lm4;
hence
a,
p,
q,
r are_coplanar
by Th7;
verum end; assume A14:
not
p,
q,
r are_collinear
;
a,p,q,r are_coplanar
a <> b
by A1, ANPROJ_2:def 7;
then
( not
a,
b,
p are_collinear or not
a,
b,
q are_collinear or not
a,
b,
r are_collinear )
by A14, ANPROJ_2:def 8;
hence
a,
p,
q,
r are_coplanar
by A8, A11, A5, Th1;
verum
hence
a,p,q,r are_coplanar
by Th6; verum