let FCPS be up-3-dimensional CollProjectiveSpace; for p, q, r, a, b, c, s being Element of FCPS st not p,q,r is_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 p, q, r, a, b, c, s be Element of FCPS; ( not p,q,r is_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 is_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
b,
b,
a is_collinear
by ANPROJ_2:def 7;
then A6:
b,
a,
c,
b are_coplanar
by Th10;
A7:
b,
a,
c,
r are_coplanar
by A3, Th11;
assume A8:
not
a,
b,
c is_collinear
;
a,b,c,s are_coplanar then A9:
not
b,
a,
c is_collinear
by Th1;
a,
p,
q,
r are_coplanar
by A2, A3, A4, A8, Lm5;
then A10:
p,
q,
r,
a are_coplanar
by Th11;
A11:
c,
a,
b,
r are_coplanar
by A3, Th11;
A12:
not
c,
a,
b is_collinear
by A8, Th1;
(
c,
a,
b,
p are_coplanar &
c,
a,
b,
q are_coplanar )
by A2, A4, Th11;
then
c,
p,
q,
r are_coplanar
by A12, A11, Lm5;
then A13:
p,
q,
r,
c are_coplanar
by Th11;
(
b,
a,
c,
p are_coplanar &
b,
a,
c,
q are_coplanar )
by A2, A4, Th11;
then
p,
q,
r,
b are_coplanar
by A9, A6, A7, Th12;
hence
a,
b,
c,
s are_coplanar
by A1, A5, A10, A13, Th12;
verum end;
hence
a,b,c,s are_coplanar
by Th10; verum