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