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