let FCPS be up-3-dimensional CollProjectiveSpace; for a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar holds
p,q,r,s are_coplanar
let a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar implies p,q,r,s 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
and
A5:
a,b,c,s are_coplanar
; p,q,r,s are_coplanar
A6:
a,b,p,q are_coplanar
by A1, A2, A3, Lm4;
A7:
a,b,q,r are_coplanar
by A1, A3, A4, Lm4;
A8:
a,b,p,r are_coplanar
by A1, A2, A4, Lm4;
A9:
a,b,q,s are_coplanar
by A1, A3, A5, Lm4;
A10:
now ( not a,b,q are_collinear implies p,q,r,s are_coplanar )A11:
q,
a,
b,
r are_coplanar
by A7, Th7;
assume A12:
not
a,
b,
q are_collinear
;
p,q,r,s are_coplanar then A13:
not
q,
a,
b are_collinear
by Th1;
A14:
q,
a,
b,
p are_coplanar
by A6, Th7;
then A15:
q,
a,
p,
r are_coplanar
by A13, A11, Lm4;
A16:
q,
a,
b,
s are_coplanar
by A9, Th7;
then A17:
q,
a,
p,
s are_coplanar
by A13, A14, Lm4;
A18:
now ( not q,a,p are_collinear implies p,q,r,s are_coplanar )assume
not
q,
a,
p are_collinear
;
p,q,r,s are_coplanar then A19:
not
q,
p,
a are_collinear
by Th1;
(
q,
p,
a,
r are_coplanar &
q,
p,
a,
s are_coplanar )
by A15, A17, Th7;
then
q,
p,
r,
s are_coplanar
by A19, Lm4;
hence
p,
q,
r,
s are_coplanar
by Th7;
verum end; A20:
q,
a,
r,
s are_coplanar
by A13, A11, A16, Lm4;
A21:
now ( not q,a,r are_collinear implies p,q,r,s are_coplanar )assume
not
q,
a,
r are_collinear
;
p,q,r,s are_coplanar then A22:
not
q,
r,
a are_collinear
by Th1;
(
q,
r,
a,
p are_coplanar &
q,
r,
a,
s are_coplanar )
by A15, A20, Th7;
then
q,
r,
p,
s are_coplanar
by A22, Lm4;
hence
p,
q,
r,
s are_coplanar
by Th7;
verum end; A23:
q <> a
by A12, ANPROJ_2:def 7;
now ( q,a,p are_collinear & q,a,r are_collinear implies p,q,r,s are_coplanar )assume
(
q,
a,
p are_collinear &
q,
a,
r are_collinear )
;
p,q,r,s are_coplanar then
q,
p,
r are_collinear
by A23, COLLSP:6;
then
p,
q,
r are_collinear
by Th1;
hence
p,
q,
r,
s are_coplanar
by Th6;
verum end; hence
p,
q,
r,
s are_coplanar
by A18, A21;
verum end;
A24:
a,b,r,s are_coplanar
by A1, A4, A5, Lm4;
A25:
now ( not a,b,r are_collinear implies p,q,r,s are_coplanar )A26:
r,
a,
b,
q are_coplanar
by A7, Th7;
assume A27:
not
a,
b,
r are_collinear
;
p,q,r,s are_coplanar then A28:
not
r,
a,
b are_collinear
by Th1;
A29:
r,
a,
b,
p are_coplanar
by A8, Th7;
then A30:
r,
a,
p,
q are_coplanar
by A28, A26, Lm4;
A31:
r,
a,
b,
s are_coplanar
by A24, Th7;
then A32:
r,
a,
p,
s are_coplanar
by A28, A29, Lm4;
A33:
now ( not r,a,p are_collinear implies p,q,r,s are_coplanar )assume
not
r,
a,
p are_collinear
;
p,q,r,s are_coplanar then A34:
not
r,
p,
a are_collinear
by Th1;
(
r,
p,
a,
q are_coplanar &
r,
p,
a,
s are_coplanar )
by A30, A32, Th7;
then
r,
p,
q,
s are_coplanar
by A34, Lm4;
hence
p,
q,
r,
s are_coplanar
by Th7;
verum end; A35:
r,
a,
q,
s are_coplanar
by A28, A26, A31, Lm4;
A36:
now ( not r,a,q are_collinear implies p,q,r,s are_coplanar )assume
not
r,
a,
q are_collinear
;
p,q,r,s are_coplanar then A37:
not
r,
q,
a are_collinear
by Th1;
(
r,
q,
a,
p are_coplanar &
r,
q,
a,
s are_coplanar )
by A30, A35, Th7;
then
r,
q,
p,
s are_coplanar
by A37, Lm4;
hence
p,
q,
r,
s are_coplanar
by Th7;
verum end; A38:
r <> a
by A27, ANPROJ_2:def 7;
now ( r,a,p are_collinear & r,a,q are_collinear implies p,q,r,s are_coplanar )assume
(
r,
a,
p are_collinear &
r,
a,
q are_collinear )
;
p,q,r,s are_coplanar then
r,
p,
q are_collinear
by A38, COLLSP:6;
then
p,
q,
r are_collinear
by Th1;
hence
p,
q,
r,
s are_coplanar
by Th6;
verum end; hence
p,
q,
r,
s are_coplanar
by A33, A36;
verum end;
A39:
a,b,p,s are_coplanar
by A1, A2, A5, Lm4;
A40:
now ( not a,b,p are_collinear implies p,q,r,s are_coplanar )A41:
p,
a,
b,
r are_coplanar
by A8, Th7;
assume A42:
not
a,
b,
p are_collinear
;
p,q,r,s are_coplanar then A43:
not
p,
a,
b are_collinear
by Th1;
A44:
p,
a,
b,
q are_coplanar
by A6, Th7;
then A45:
p,
a,
q,
r are_coplanar
by A43, A41, Lm4;
A46:
p,
a,
b,
s are_coplanar
by A39, Th7;
then A47:
p,
a,
q,
s are_coplanar
by A43, A44, Lm4;
A48:
now ( not p,a,q are_collinear implies p,q,r,s are_coplanar )assume
not
p,
a,
q are_collinear
;
p,q,r,s are_coplanar then A49:
not
p,
q,
a are_collinear
by Th1;
(
p,
q,
a,
r are_coplanar &
p,
q,
a,
s are_coplanar )
by A45, A47, Th7;
hence
p,
q,
r,
s are_coplanar
by A49, Lm4;
verum end; A50:
p,
a,
r,
s are_coplanar
by A43, A41, A46, Lm4;
A51:
now ( not p,a,r are_collinear implies p,q,r,s are_coplanar )assume
not
p,
a,
r are_collinear
;
p,q,r,s are_coplanar then A52:
not
p,
r,
a are_collinear
by Th1;
(
p,
r,
a,
q are_coplanar &
p,
r,
a,
s are_coplanar )
by A45, A50, Th7;
then
p,
r,
q,
s are_coplanar
by A52, Lm4;
hence
p,
q,
r,
s are_coplanar
by Th7;
verum end; A53:
p <> a
by A42, ANPROJ_2:def 7;
now ( p,a,q are_collinear & p,a,r are_collinear implies p,q,r,s are_coplanar )assume
(
p,
a,
q are_collinear &
p,
a,
r are_collinear )
;
p,q,r,s are_coplanar then
p,
q,
r are_collinear
by A53, COLLSP:6;
hence
p,
q,
r,
s are_coplanar
by Th6;
verum end; hence
p,
q,
r,
s are_coplanar
by A48, A51;
verum end;
A54:
a <> b
by A1, ANPROJ_2:def 7;
now ( a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear implies p,q,r,s are_coplanar )assume
(
a,
b,
p are_collinear &
a,
b,
q are_collinear &
a,
b,
r are_collinear )
;
p,q,r,s are_coplanar then
p,
q,
r are_collinear
by A54, ANPROJ_2:def 8;
hence
p,
q,
r,
s are_coplanar
by Th6;
verum end;
hence
p,q,r,s are_coplanar
by A40, A10, A25; verum