let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: 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; :: thesis: ( 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 A1:
( 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 )
; :: thesis: a,b,c,s are_coplanar
now assume A2:
not
a,
b,
c is_collinear
;
:: thesis: a,b,c,s are_coplanar then A3:
a,
p,
q,
r are_coplanar
by A1, Lm5;
A4:
not
b,
a,
c is_collinear
by A2, Th1;
b,
b,
a is_collinear
by ANPROJ_2:def 7;
then A5:
(
b,
a,
c,
b are_coplanar &
b,
a,
c,
p are_coplanar &
b,
a,
c,
q are_coplanar &
b,
a,
c,
r are_coplanar )
by A1, Th10, Th11;
A6:
not
c,
a,
b is_collinear
by A2, Th1;
(
c,
a,
b,
p are_coplanar &
c,
a,
b,
q are_coplanar &
c,
a,
b,
r are_coplanar )
by A1, Th11;
then
c,
p,
q,
r are_coplanar
by A6, Lm5;
then
(
p,
q,
r,
a are_coplanar &
p,
q,
r,
b are_coplanar &
p,
q,
r,
c are_coplanar )
by A3, A4, A5, Th11, Th12;
hence
a,
b,
c,
s are_coplanar
by A1, Th12;
:: thesis: verum end;
hence
a,b,c,s are_coplanar
by Th10; :: thesis: verum