:: PROJDES1 semantic presentation

begin


theorem Th1: :: PROJDES1:1
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c being Element of FCPS st a,b,c is_collinear holds
( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c being Element of FCPS st a,b,c is_collinear holds
( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )
let a, b, c be Element of FCPS; ::_thesis: ( a,b,c is_collinear implies ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) )
assume A1: a,b,c is_collinear ; ::_thesis: ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )
then  b,a,c is_collinear by COLLSP:4;
then A2: b,c,a is_collinear by COLLSP:4;
 a,c,b is_collinear by A1, COLLSP:4;
hence  ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) by A2, COLLSP:4; ::_thesis: verum
end;

theorem :: PROJDES1:2
for FCPS being up-3-dimensional CollProjectiveSpace
for p being Element of FCPS holds
not for q, r being Element of FCPS holds p,q,r is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for p being Element of FCPS holds
not for q, r being Element of FCPS holds p,q,r is_collinear
let p be Element of FCPS; ::_thesis: not for q, r being Element of FCPS holds p,q,r is_collinear
consider q being Element of FCPS such that
A1: p <> q and
 p <> q and
 p,p,q is_collinear by ANPROJ_2:def_10;
 not for r being Element of FCPS holds p,q,r is_collinear by A1, COLLSP:12;
hence  not for q, r being Element of FCPS holds p,q,r is_collinear ; ::_thesis: verum
end;

theorem :: PROJDES1:3
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, b9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 holds
not a,b9,c is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, b9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 holds
not a,b9,c is_collinear
let a, b, c, b9 be Element of FCPS; ::_thesis: ( not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 implies not a,b9,c is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: a,b,b9 is_collinear and
A3: a <> b9 ; ::_thesis: not a,b9,c is_collinear
assume A4: a,b9,c is_collinear ; ::_thesis: contradiction
 a,b9,b is_collinear by A2, Th1;
hence  contradiction by A1, A3, A4, COLLSP:6; ::_thesis: verum
end;

theorem :: PROJDES1:4
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds
a = d
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds
a = d
let a, b, c, d be Element of FCPS; ::_thesis: ( not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear implies a = d )
assume that
A1: not a,b,c is_collinear and
A2: ( a,b,d is_collinear & a,c,d is_collinear ) ; ::_thesis: a = d
assume A3: not a = d ; ::_thesis: contradiction
A4: a,d,a is_collinear by ANPROJ_2:def_7;
 ( a,d,b is_collinear & a,d,c is_collinear ) by A2, Th1;
hence  contradiction by A1, A3, A4, ANPROJ_2:def_8; ::_thesis: verum
end;

theorem Th5: :: PROJDES1:5
for FCPS being up-3-dimensional CollProjectiveSpace
for o, a, d, d9, a9, s being Element of FCPS st not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,s is_collinear & o,a,a9 is_collinear & o <> a9 holds
s <> d
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for o, a, d, d9, a9, s being Element of FCPS st not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,s is_collinear & o,a,a9 is_collinear & o <> a9 holds
s <> d
let o, a, d, d9, a9, s be Element of FCPS; ::_thesis: ( not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,s is_collinear & o,a,a9 is_collinear & o <> a9 implies s <> d )
assume that
A1: not o,a,d is_collinear and
A2: o,d,d9 is_collinear and
A3: d <> d9 and
A4: a9,d9,s is_collinear and
A5: o,a,a9 is_collinear and
A6: o <> a9 ; ::_thesis: s <> d
assume  not s <> d ; ::_thesis: contradiction
then A7: d,d9,a9 is_collinear by A4, Th1;
 d,d9,o is_collinear by A2, Th1;
then  d,o,a9 is_collinear by A3, A7, COLLSP:6;
then A8: o,a9,d is_collinear by Th1;
 o,a9,a is_collinear by A5, Th1;
hence  contradiction by A1, A6, A8, COLLSP:6; ::_thesis: verum
end;

Lm1:  for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, b9, c9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 holds
b9 <> c9
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, b9, c9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 holds
b9 <> c9
let a, b, c, b9, c9 be Element of FCPS; ::_thesis: ( not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 implies b9 <> c9 )
assume that
A1: not a,b,c is_collinear and
A2: a,b,b9 is_collinear and
A3: a,c,c9 is_collinear and
A4: a <> b9 ; ::_thesis: b9 <> c9
assume  not b9 <> c9 ; ::_thesis: contradiction
then A5: a,b9,c is_collinear by A3, Th1;
 a,b9,b is_collinear by A2, Th1;
hence  contradiction by A1, A4, A5, COLLSP:6; ::_thesis: verum
end;

definition
let FCPS be up-3-dimensional CollProjectiveSpace;
let a, b, c, d be Element of FCPS;
preda,b,c,d are_coplanar  means :Def1: :: PROJDES1:def 1
 ex x being Element of FCPS st
( a,b,x is_collinear & c,d,x is_collinear );
end;

:: deftheorem Def1 defines are_coplanar PROJDES1:def_1_:_
 for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS holds
( a,b,c,d are_coplanar iff ex x being Element of FCPS st
( a,b,x is_collinear & c,d,x is_collinear ) );

theorem Th6: :: PROJDES1:6
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) holds
a,b,c,d are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) holds
a,b,c,d are_coplanar
let a, b, c, d be Element of FCPS; ::_thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
A1: now__::_thesis:_(_a,b,c_is_collinear_&_(_a,b,c_is_collinear_or_b,c,d_is_collinear_or_c,d,a_is_collinear_or_d,a,b_is_collinear_)_implies_a,b,c,d_are_coplanar_)
A2: c,d,c is_collinear by ANPROJ_2:def_7;
assume  a,b,c is_collinear ; ::_thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
hence  ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar ) by A2, Def1; ::_thesis: verum
end;
A3: now__::_thesis:_(_c,d,a_is_collinear_&_(_a,b,c_is_collinear_or_b,c,d_is_collinear_or_c,d,a_is_collinear_or_d,a,b_is_collinear_)_implies_a,b,c,d_are_coplanar_)
A4: a,b,a is_collinear by ANPROJ_2:def_7;
assume  c,d,a is_collinear ; ::_thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
hence  ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar ) by A4, Def1; ::_thesis: verum
end;
A5: now__::_thesis:_(_d,a,b_is_collinear_&_(_a,b,c_is_collinear_or_b,c,d_is_collinear_or_c,d,a_is_collinear_or_d,a,b_is_collinear_)_implies_a,b,c,d_are_coplanar_)
assume  d,a,b is_collinear ; ::_thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
then A6: a,b,d is_collinear by Th1;
 c,d,d is_collinear by ANPROJ_2:def_7;
hence  ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar ) by A6, Def1; ::_thesis: verum
end;
A7: now__::_thesis:_(_b,c,d_is_collinear_&_(_a,b,c_is_collinear_or_b,c,d_is_collinear_or_c,d,a_is_collinear_or_d,a,b_is_collinear_)_implies_a,b,c,d_are_coplanar_)
assume  b,c,d is_collinear ; ::_thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
then A8: c,d,b is_collinear by Th1;
 a,b,b is_collinear by ANPROJ_2:def_7;
hence  ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar ) by A8, Def1; ::_thesis: verum
end;
assume  ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) ; ::_thesis: a,b,c,d are_coplanar
hence  a,b,c,d are_coplanar by A1, A7, A3, A5; ::_thesis: verum
end;

Lm2:  for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
b,a,c,d are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
b,a,c,d are_coplanar
let a, b, c, d be Element of FCPS; ::_thesis: ( a,b,c,d are_coplanar implies b,a,c,d are_coplanar )
assume  a,b,c,d are_coplanar ; ::_thesis: b,a,c,d are_coplanar
then consider x being Element of FCPS such that
A1: a,b,x is_collinear and
A2: c,d,x is_collinear by Def1;
 b,a,x is_collinear by A1, Th1;
hence  b,a,c,d are_coplanar by A2, Def1; ::_thesis: verum
end;

Lm3:  for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
b,c,d,a are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
b,c,d,a are_coplanar
let a, b, c, d be Element of FCPS; ::_thesis: ( a,b,c,d are_coplanar implies b,c,d,a are_coplanar )
assume  a,b,c,d are_coplanar ; ::_thesis: b,c,d,a are_coplanar
then consider x being Element of FCPS such that
A1: ( a,b,x is_collinear & c,d,x is_collinear ) by Def1;
 ( b,x,a is_collinear & x,c,d is_collinear ) by A1, Th1;
then consider y being Element of FCPS such that
A2: b,c,y is_collinear and
A3: a,d,y is_collinear by ANPROJ_2:def_9;
 d,a,y is_collinear by A3, Th1;
hence  b,c,d,a are_coplanar by A2, Def1; ::_thesis: verum
end;

theorem Th7: :: PROJDES1:7
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar )
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar )
let a, b, c, d be Element of FCPS; ::_thesis: ( a,b,c,d are_coplanar implies ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar ) )
assume A1: a,b,c,d are_coplanar ; ::_thesis: ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar )
then A2: b,a,c,d are_coplanar by Lm2;
then  a,c,d,b are_coplanar by Lm3;
then A3: c,d,b,a are_coplanar by Lm3;
then A4: d,b,a,c are_coplanar by Lm3;
then  b,d,a,c are_coplanar by Lm2;
then A5: d,a,c,b are_coplanar by Lm3;
then A6: a,c,b,d are_coplanar by Lm3;
then  c,a,b,d are_coplanar by Lm2;
then A7: a,b,d,c are_coplanar by Lm3;
then A8: b,d,c,a are_coplanar by Lm3;
then A9: d,c,a,b are_coplanar by Lm3;
then  c,d,a,b are_coplanar by Lm2;
then A10: d,a,b,c are_coplanar by Lm3;
then  a,d,b,c are_coplanar by Lm2;
then  d,b,c,a are_coplanar by Lm3;
then  b,c,a,d are_coplanar by Lm3;
hence  ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, Lm2, Lm3; ::_thesis: verum
end;

Lm4:  for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, p, q being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,p,q are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, p, q being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,p,q are_coplanar
let a, b, c, p, q be Element of FCPS; ::_thesis: ( not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar implies a,b,p,q are_coplanar )
assume that
A1: not a,b,c is_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar ; ::_thesis: a,b,p,q are_coplanar
consider x being Element of FCPS such that
A4: a,b,x is_collinear and
A5: c,p,x is_collinear by A2, Def1;
consider y being Element of FCPS such that
A6: a,b,y is_collinear and
A7: c,q,y is_collinear by A3, Def1;
A8: now__::_thesis:_(_a_<>_b_implies_a,b,p,q_are_coplanar_)
assume A9: a <> b ; ::_thesis: a,b,p,q are_coplanar
 ( b,a,x is_collinear & b,a,y is_collinear ) by A4, A6, Th1;
then  b,x,y is_collinear by A9, COLLSP:6;
then A10: x,y,b is_collinear by Th1;
 a,x,y is_collinear by A4, A6, A9, COLLSP:6;
then A11: x,y,a is_collinear by Th1;
A12: now__::_thesis:_(_x_<>_y_implies_a,b,p,q_are_coplanar_)
 p,c,x is_collinear by A5, Th1;
then consider z being Element of FCPS such that
A13: p,q,z is_collinear and
A14: x,y,z is_collinear by A7, ANPROJ_2:def_9;
assume  x <> y ; ::_thesis: a,b,p,q are_coplanar
then  a,b,z is_collinear by A11, A10, A14, ANPROJ_2:def_8;
hence  a,b,p,q are_coplanar by A13, Def1; ::_thesis: verum
end;
now__::_thesis:_(_x_=_y_implies_a,b,p,q_are_coplanar_)
assume  x = y ; ::_thesis: a,b,p,q are_coplanar
then A15: x,c,q is_collinear by A7, Th1;
 x,c,p is_collinear by A5, Th1;
then  x,p,q is_collinear by A1, A4, A15, COLLSP:6;
then  p,q,x is_collinear by Th1;
hence  a,b,p,q are_coplanar by A4, Def1; ::_thesis: verum
end;
hence  a,b,p,q are_coplanar by A12; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_implies_a,b,p,q_are_coplanar_)
assume  a = b ; ::_thesis: a,b,p,q are_coplanar
then  a,b,p is_collinear by ANPROJ_2:def_7;
hence  a,b,p,q are_coplanar by Th6; ::_thesis: verum
end;
hence  a,b,p,q are_coplanar by A8; ::_thesis: verum
end;

theorem Th8: :: PROJDES1:8
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar holds
p,q,r,s are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, p, q, r, s 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 & 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; ::_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 & a,b,c,s are_coplanar implies p,q,r,s are_coplanar )
assume that
A1: not a,b,c is_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 ; ::_thesis: 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__::_thesis:_(_not_a,b,q_is_collinear_implies_p,q,r,s_are_coplanar_)
A11: q,a,b,r are_coplanar by A7, Th7;
assume A12: not a,b,q is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A13: not q,a,b is_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__::_thesis:_(_not_q,a,p_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not q,a,p is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A19: not q,p,a is_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; ::_thesis: verum
end;
A20: q,a,r,s are_coplanar by A13, A11, A16, Lm4;
A21: now__::_thesis:_(_not_q,a,r_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not q,a,r is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A22: not q,r,a is_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; ::_thesis: verum
end;
A23: q <> a by A12, ANPROJ_2:def_7;
now__::_thesis:_(_q,a,p_is_collinear_&_q,a,r_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  ( q,a,p is_collinear & q,a,r is_collinear ) ; ::_thesis: p,q,r,s are_coplanar
then  q,p,r is_collinear by A23, COLLSP:6;
then  p,q,r is_collinear by Th1;
hence  p,q,r,s are_coplanar by Th6; ::_thesis: verum
end;
hence  p,q,r,s are_coplanar by A18, A21; ::_thesis: verum
end;
A24: a,b,r,s are_coplanar by A1, A4, A5, Lm4;
A25: now__::_thesis:_(_not_a,b,r_is_collinear_implies_p,q,r,s_are_coplanar_)
A26: r,a,b,q are_coplanar by A7, Th7;
assume A27: not a,b,r is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A28: not r,a,b is_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__::_thesis:_(_not_r,a,p_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not r,a,p is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A34: not r,p,a is_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; ::_thesis: verum
end;
A35: r,a,q,s are_coplanar by A28, A26, A31, Lm4;
A36: now__::_thesis:_(_not_r,a,q_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not r,a,q is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A37: not r,q,a is_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; ::_thesis: verum
end;
A38: r <> a by A27, ANPROJ_2:def_7;
now__::_thesis:_(_r,a,p_is_collinear_&_r,a,q_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  ( r,a,p is_collinear & r,a,q is_collinear ) ; ::_thesis: p,q,r,s are_coplanar
then  r,p,q is_collinear by A38, COLLSP:6;
then  p,q,r is_collinear by Th1;
hence  p,q,r,s are_coplanar by Th6; ::_thesis: verum
end;
hence  p,q,r,s are_coplanar by A33, A36; ::_thesis: verum
end;
A39: a,b,p,s are_coplanar by A1, A2, A5, Lm4;
A40: now__::_thesis:_(_not_a,b,p_is_collinear_implies_p,q,r,s_are_coplanar_)
A41: p,a,b,r are_coplanar by A8, Th7;
assume A42: not a,b,p is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A43: not p,a,b is_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__::_thesis:_(_not_p,a,q_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not p,a,q is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A49: not p,q,a is_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; ::_thesis: verum
end;
A50: p,a,r,s are_coplanar by A43, A41, A46, Lm4;
A51: now__::_thesis:_(_not_p,a,r_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  not p,a,r is_collinear ; ::_thesis: p,q,r,s are_coplanar
then A52: not p,r,a is_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; ::_thesis: verum
end;
A53: p <> a by A42, ANPROJ_2:def_7;
now__::_thesis:_(_p,a,q_is_collinear_&_p,a,r_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  ( p,a,q is_collinear & p,a,r is_collinear ) ; ::_thesis: p,q,r,s are_coplanar
then  p,q,r is_collinear by A53, COLLSP:6;
hence  p,q,r,s are_coplanar by Th6; ::_thesis: verum
end;
hence  p,q,r,s are_coplanar by A48, A51; ::_thesis: verum
end;
A54: a <> b by A1, ANPROJ_2:def_7;
now__::_thesis:_(_a,b,p_is_collinear_&_a,b,q_is_collinear_&_a,b,r_is_collinear_implies_p,q,r,s_are_coplanar_)
assume  ( a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear ) ; ::_thesis: p,q,r,s are_coplanar
then  p,q,r is_collinear by A54, ANPROJ_2:def_8;
hence  p,q,r,s are_coplanar by Th6; ::_thesis: verum
end;
hence  p,q,r,s are_coplanar by A40, A10, A25; ::_thesis: verum
end;

Lm5:  for FCPS being up-3-dimensional CollProjectiveSpace
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
proof
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 that
A1: not a,b,c is_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 ; ::_thesis: a,p,q,r are_coplanar
now__::_thesis:_(_not_p,q,r_is_collinear_implies_a,p,q,r_are_coplanar_)
A5: now__::_thesis:_(_not_a,r,b_is_collinear_implies_a,p,q,r_are_coplanar_)
 a,b,r,q are_coplanar by A1, A3, A4, Lm4;
then A6: a,r,b,q are_coplanar by Th7;
 a,b,r,p are_coplanar by A1, A2, A4, Lm4;
then A7: a,r,b,p are_coplanar by Th7;
assume  not a,r,b is_collinear ; ::_thesis: a,p,q,r are_coplanar
then  a,r,p,q are_coplanar by A7, A6, Lm4;
hence  a,p,q,r are_coplanar by Th7; ::_thesis: verum
end;
A8: now__::_thesis:_(_not_a,p,b_is_collinear_implies_a,p,q,r_are_coplanar_)
 a,b,p,r are_coplanar by A1, A2, A4, Lm4;
then A9: a,p,b,r are_coplanar by Th7;
 a,b,p,q are_coplanar by A1, A2, A3, Lm4;
then A10: a,p,b,q are_coplanar by Th7;
assume  not a,p,b is_collinear ; ::_thesis: a,p,q,r are_coplanar
hence  a,p,q,r are_coplanar by A10, A9, Lm4; ::_thesis: verum
end;
A11: now__::_thesis:_(_not_a,q,b_is_collinear_implies_a,p,q,r_are_coplanar_)
 a,b,q,r are_coplanar by A1, A3, A4, Lm4;
then A12: a,q,b,r are_coplanar by Th7;
 a,b,q,p are_coplanar by A1, A2, A3, Lm4;
then A13: a,q,b,p are_coplanar by Th7;
assume  not a,q,b is_collinear ; ::_thesis: a,p,q,r are_coplanar
then  a,q,p,r are_coplanar by A13, A12, Lm4;
hence  a,p,q,r are_coplanar by Th7; ::_thesis: verum
end;
assume A14: not p,q,r is_collinear ; ::_thesis: a,p,q,r are_coplanar
 a <> b by A1, ANPROJ_2:def_7;
then  ( not a,b,p is_collinear or not a,b,q is_collinear or not a,b,r is_collinear ) by A14, ANPROJ_2:def_8;
hence  a,p,q,r are_coplanar by A8, A11, A5, Th1; ::_thesis: verum
end;
hence  a,p,q,r are_coplanar by Th6; ::_thesis: verum
end;

theorem :: PROJDES1:9
for FCPS being 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
proof
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 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 ; ::_thesis: a,b,c,s are_coplanar
now__::_thesis:_(_not_a,b,c_is_collinear_implies_a,b,c,s_are_coplanar_)
 b,b,a is_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 is_collinear ; ::_thesis: 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 Th7;
A11: c,a,b,r are_coplanar by A3, Th7;
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, 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; ::_thesis: verum
end;
hence  a,b,c,s are_coplanar by Th6; ::_thesis: verum
end;

Lm6:  for FCPS being up-3-dimensional CollProjectiveSpace
for p, q, r, a, b being Element of FCPS st p <> q & p,q,r is_collinear & a,b,p,q are_coplanar holds
a,b,p,r are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for p, q, r, a, b being Element of FCPS st p <> q & p,q,r is_collinear & a,b,p,q are_coplanar holds
a,b,p,r are_coplanar
let p, q, r, a, b be Element of FCPS; ::_thesis: ( p <> q & p,q,r is_collinear & a,b,p,q are_coplanar implies a,b,p,r are_coplanar )
assume that
A1: ( p <> q & p,q,r is_collinear ) and
A2: a,b,p,q are_coplanar ; ::_thesis: a,b,p,r are_coplanar
consider x being Element of FCPS such that
A3: a,b,x is_collinear and
A4: p,q,x is_collinear by A2, Def1;
 p,r,x is_collinear by A1, A4, COLLSP:6;
hence  a,b,p,r are_coplanar by A3, Def1; ::_thesis: verum
end;

theorem Th10: :: PROJDES1:10
for FCPS being up-3-dimensional CollProjectiveSpace
for p, q, r, a, b, c being Element of FCPS st p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,c,r are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for p, q, r, a, b, c being Element of FCPS st p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,c,r are_coplanar
let p, q, r, a, b, c be Element of FCPS; ::_thesis: ( p <> q & p,q,r is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar implies a,b,c,r are_coplanar )
assume that
A1: p <> q and
A2: p,q,r is_collinear and
A3: a,b,c,p are_coplanar and
A4: a,b,c,q are_coplanar ; ::_thesis: a,b,c,r are_coplanar
A5: q,p,r is_collinear by A2, Th1;
now__::_thesis:_(_not_a,b,c_is_collinear_implies_a,b,c,r_are_coplanar_)
assume A6: not a,b,c is_collinear ; ::_thesis: a,b,c,r are_coplanar
then  a,b,p,q are_coplanar by A3, A4, Lm4;
then A7: a,b,p,r are_coplanar by A1, A2, Lm6;
A8: now__::_thesis:_(_not_a,b,p_is_collinear_implies_a,b,c,r_are_coplanar_)
 b,a,b is_collinear by ANPROJ_2:def_7;
then A9: a,b,p,b are_coplanar by Th6;
 a,a,b is_collinear by ANPROJ_2:def_7;
then A10: a,b,p,a are_coplanar by Th6;
assume A11: not a,b,p is_collinear ; ::_thesis: a,b,c,r are_coplanar
 a,b,p,c are_coplanar by A3, Th7;
hence  a,b,c,r are_coplanar by A7, A11, A10, A9, Th8; ::_thesis: verum
end;
 a,b,q,p are_coplanar by A3, A4, A6, Lm4;
then A12: a,b,q,r are_coplanar by A1, A5, Lm6;
A13: now__::_thesis:_(_not_a,b,q_is_collinear_implies_a,b,c,r_are_coplanar_)
 b,a,b is_collinear by ANPROJ_2:def_7;
then A14: a,b,q,b are_coplanar by Th6;
 a,a,b is_collinear by ANPROJ_2:def_7;
then A15: a,b,q,a are_coplanar by Th6;
assume A16: not a,b,q is_collinear ; ::_thesis: a,b,c,r are_coplanar
 a,b,q,c are_coplanar by A4, Th7;
hence  a,b,c,r are_coplanar by A12, A16, A15, A14, Th8; ::_thesis: verum
end;
now__::_thesis:_(_a,b,p_is_collinear_&_a,b,q_is_collinear_implies_a,b,c,r_are_coplanar_)
assume  ( a,b,p is_collinear & a,b,q is_collinear ) ; ::_thesis: a,b,c,r are_coplanar
then  a,b,r is_collinear by A1, A2, COLLSP:9;
then  r,a,b is_collinear by Th1;
hence  a,b,c,r are_coplanar by Th6; ::_thesis: verum
end;
hence  a,b,c,r are_coplanar by A8, A13; ::_thesis: verum
end;
hence  a,b,c,r are_coplanar by Th6; ::_thesis: verum
end;

theorem :: PROJDES1:11
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar holds
ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear )
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar holds
ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear )
let a, b, c, p, q, r, s 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 & a,b,c,s are_coplanar implies ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear ) )
assume  ( not a,b,c is_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 ) ; ::_thesis: ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear )
then  p,q,r,s are_coplanar by Th8;
then consider x being Element of FCPS such that
A1: ( p,q,x is_collinear & r,s,x is_collinear ) by Def1;
take  x ; ::_thesis: ( p,q,x is_collinear & r,s,x is_collinear )
thus  ( p,q,x is_collinear & r,s,x is_collinear ) by A1; ::_thesis: verum
end;

theorem Th12: :: PROJDES1:12
for FCPS being up-3-dimensional CollProjectiveSpace holds
not for a, b, c, d being Element of FCPS holds a,b,c,d are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: not for a, b, c, d being Element of FCPS holds a,b,c,d are_coplanar
consider a, b, c, d being Element of FCPS such that
A1: for x being Element of FCPS holds
( not a,b,x is_collinear or not c,d,x is_collinear ) by ANPROJ_2:def_14;
take  a ; ::_thesis: not for b, c, d being Element of FCPS holds a,b,c,d are_coplanar
take  b ; ::_thesis: not for c, d being Element of FCPS holds a,b,c,d are_coplanar
take  c ; ::_thesis: not for d being Element of FCPS holds a,b,c,d are_coplanar
take  d ; ::_thesis: not a,b,c,d are_coplanar
thus  not a,b,c,d are_coplanar by A1, Def1; ::_thesis: verum
end;

theorem Th13: :: PROJDES1:13
for FCPS being up-3-dimensional CollProjectiveSpace
for p, q, r being Element of FCPS st not p,q,r is_collinear holds
ex s being Element of FCPS st not p,q,r,s are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for p, q, r being Element of FCPS st not p,q,r is_collinear holds
ex s being Element of FCPS st not p,q,r,s are_coplanar
let p, q, r be Element of FCPS; ::_thesis: ( not p,q,r is_collinear implies ex s being Element of FCPS st not p,q,r,s are_coplanar )
assume A1: not p,q,r is_collinear ; ::_thesis: not for s being Element of FCPS holds p,q,r,s are_coplanar
consider a, b, c, d being Element of FCPS such that
A2: not a,b,c,d are_coplanar by Th12;
assume A3: for s being Element of FCPS holds p,q,r,s are_coplanar ; ::_thesis: contradiction
then A4: ( p,q,r,c are_coplanar & p,q,r,d are_coplanar ) ;
 ( p,q,r,a are_coplanar & p,q,r,b are_coplanar ) by A3;
hence  contradiction by A1, A2, A4, Th8; ::_thesis: verum
end;

theorem Th14: :: PROJDES1:14
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS st ( a = b or a = c or b = c or a = d or b = d or d = c ) holds
a,b,c,d are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of FCPS st ( a = b or a = c or b = c or a = d or b = d or d = c ) holds
a,b,c,d are_coplanar
let a, b, c, d be Element of FCPS; ::_thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )
A1: now__::_thesis:_(_(_a_=_b_or_a_=_c_or_b_=_c_)_&_(_a_=_b_or_a_=_c_or_b_=_c_or_a_=_d_or_b_=_d_or_d_=_c_)_implies_a,b,c,d_are_coplanar_)
assume  ( a = b or a = c or b = c ) ; ::_thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )
then  a,b,c is_collinear by ANPROJ_2:def_7;
hence  ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; ::_thesis: verum
end;
A2: now__::_thesis:_(_(_a_=_d_or_b_=_d_)_&_(_a_=_b_or_a_=_c_or_b_=_c_or_a_=_d_or_b_=_d_or_d_=_c_)_implies_a,b,c,d_are_coplanar_)
assume  ( a = d or b = d ) ; ::_thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )
then  d,a,b is_collinear by ANPROJ_2:def_7;
hence  ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; ::_thesis: verum
end;
A3: now__::_thesis:_(_d_=_c_&_(_a_=_b_or_a_=_c_or_b_=_c_or_a_=_d_or_b_=_d_or_d_=_c_)_implies_a,b,c,d_are_coplanar_)
assume  d = c ; ::_thesis: ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar )
then  b,c,d is_collinear by ANPROJ_2:def_7;
hence  ( ( a = b or a = c or b = c or a = d or b = d or d = c ) implies a,b,c,d are_coplanar ) by Th6; ::_thesis: verum
end;
assume  ( a = b or a = c or b = c or a = d or b = d or d = c ) ; ::_thesis: a,b,c,d are_coplanar
hence  a,b,c,d are_coplanar by A1, A2, A3; ::_thesis: verum
end;

theorem Th15: :: PROJDES1:15
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, o, a9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & a <> a9 holds
not a,b,c,a9 are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, o, a9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & a <> a9 holds
not a,b,c,a9 are_coplanar
let a, b, c, o, a9 be Element of FCPS; ::_thesis: ( not a,b,c,o are_coplanar & o,a,a9 is_collinear & a <> a9 implies not a,b,c,a9 are_coplanar )
assume that
A1: not a,b,c,o are_coplanar and
A2: o,a,a9 is_collinear and
A3: a <> a9 ; ::_thesis: not a,b,c,a9 are_coplanar
assume A4: a,b,c,a9 are_coplanar ; ::_thesis: contradiction
A5: a,b,c,a are_coplanar by Th14;
 a,a9,o is_collinear by A2, Th1;
hence  contradiction by A1, A3, A4, A5, Th10; ::_thesis: verum
end;

theorem Th16: :: PROJDES1:16
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, a9, b9, c9, p, q, r being Element of FCPS st not a,b,c is_collinear & not a9,b9,c9 is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar holds
p,q,r is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, a9, b9, c9, p, q, r being Element of FCPS st not a,b,c is_collinear & not a9,b9,c9 is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar holds
p,q,r is_collinear
let a, b, c, a9, b9, c9, p, q, r be Element of FCPS; ::_thesis: ( not a,b,c is_collinear & not a9,b9,c9 is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar implies p,q,r is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: not a9,b9,c9 is_collinear and
A3: ( a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar ) and
A4: ( a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar ) and
A5: not a,b,c,a9 are_coplanar ; ::_thesis: p,q,r is_collinear
 a,b,c,a are_coplanar by Th14;
then A6: p,q,r,a are_coplanar by A1, A3, Th8;
 a9,b9,c9,a9 are_coplanar by Th14;
then A7: p,q,r,a9 are_coplanar by A2, A4, Th8;
 a,b,c,c are_coplanar by Th14;
then A8: p,q,r,c are_coplanar by A1, A3, Th8;
 a,b,c,b are_coplanar by Th14;
then A9: p,q,r,b are_coplanar by A1, A3, Th8;
assume  not p,q,r is_collinear ; ::_thesis: contradiction
hence  contradiction by A5, A6, A9, A8, A7, Th8; ::_thesis: verum
end;

theorem Th17: :: PROJDES1:17
for FCPS being up-3-dimensional CollProjectiveSpace
for a, a9, o, b, c, b9, c9, p, q, r being Element of FCPS st a <> a9 & o,a,a9 is_collinear & not a,b,c,o are_coplanar & not a9,b9,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds
p,q,r is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, a9, o, b, c, b9, c9, p, q, r being Element of FCPS st a <> a9 & o,a,a9 is_collinear & not a,b,c,o are_coplanar & not a9,b9,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds
p,q,r is_collinear
let a, a9, o, b, c, b9, c9, p, q, r be Element of FCPS; ::_thesis: ( a <> a9 & o,a,a9 is_collinear & not a,b,c,o are_coplanar & not a9,b9,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear implies p,q,r is_collinear )
assume that
A1: ( a <> a9 & o,a,a9 is_collinear & not a,b,c,o are_coplanar ) and
A2: not a9,b9,c9 is_collinear and
A3: a,b,p is_collinear and
A4: a9,b9,p is_collinear and
A5: ( b,c,q is_collinear & b9,c9,q is_collinear ) and
A6: a,c,r is_collinear and
A7: a9,c9,r is_collinear ; ::_thesis: p,q,r is_collinear
A8: ( a,b,c,q are_coplanar & a9,b9,c9,q are_coplanar ) by A5, Th6;
 c9,r,a9 is_collinear by A7, Th1;
then A9: a9,b9,c9,r are_coplanar by Th6;
 p,a9,b9 is_collinear by A4, Th1;
then A10: a9,b9,c9,p are_coplanar by Th6;
 c,r,a is_collinear by A6, Th1;
then A11: a,b,c,r are_coplanar by Th6;
 p,a,b is_collinear by A3, Th1;
then A12: a,b,c,p are_coplanar by Th6;
 ( not a,b,c,a9 are_coplanar & not a,b,c is_collinear ) by A1, Th6, Th15;
hence  p,q,r is_collinear by A2, A12, A11, A10, A8, A9, Th16; ::_thesis: verum
end;

theorem Th18: :: PROJDES1:18
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d, o being Element of FCPS st not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear holds
not a,b,d,o are_coplanar
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, d, o being Element of FCPS st not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear holds
not a,b,d,o are_coplanar
let a, b, c, d, o be Element of FCPS; ::_thesis: ( not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear implies not a,b,d,o are_coplanar )
assume that
A1: not a,b,c,d are_coplanar and
A2: a,b,c,o are_coplanar and
A3: not a,b,o is_collinear ; ::_thesis: not a,b,d,o are_coplanar
assume  a,b,d,o are_coplanar ; ::_thesis: contradiction
then A4: a,b,o,d are_coplanar by Th7;
 a,b,o,c are_coplanar by A2, Th7;
hence  contradiction by A1, A3, A4, Lm4; ::_thesis: verum
end;

theorem Th19: :: PROJDES1:19
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, o, a9, b9, c9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & o <> a9 & o <> b9 & o <> c9 holds
( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar )
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, o, a9, b9, c9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & o <> a9 & o <> b9 & o <> c9 holds
( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar )
let a, b, c, o, a9, b9, c9 be Element of FCPS; ::_thesis: ( not a,b,c,o are_coplanar & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & o <> a9 & o <> b9 & o <> c9 implies ( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar ) )
assume that
A1: ( not a,b,c,o are_coplanar & o,a,a9 is_collinear ) and
A2: o,b,b9 is_collinear and
A3: o,c,c9 is_collinear and
A4: o <> a9 and
A5: o <> b9 and
A6: o <> c9 ; ::_thesis: ( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar )
 ( a,o,a9 is_collinear & not o,b,c,a are_coplanar ) by A1, Th1, Th7;
then  not o,b,c,a9 are_coplanar by A4, Th15;
then A7: not o,a9,b,c are_coplanar by Th7;
 c,o,c9 is_collinear by A3, Th1;
then  not o,a9,b,c9 are_coplanar by A6, A7, Th15;
then A8: not o,a9,c9,b are_coplanar by Th7;
 b,o,b9 is_collinear by A2, Th1;
then  not o,a9,c9,b9 are_coplanar by A5, A8, Th15;
then  not a9,b9,c9,o are_coplanar by Th7;
hence  ( not a9,b9,c9 is_collinear & not a9,b9,c9,o are_coplanar ) by Th6; ::_thesis: verum
end;

theorem Th20: :: PROJDES1:20
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, o, d, d9, a9, b9, s, t, u being Element of FCPS st a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & a,d,s is_collinear & a9,d9,s is_collinear & b,d,t is_collinear & b9,d9,t is_collinear & c,d,u is_collinear & o <> a9 & d <> d9 & o <> b9 holds
not s,t,u is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for a, b, c, o, d, d9, a9, b9, s, t, u being Element of FCPS st a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & a,d,s is_collinear & a9,d9,s is_collinear & b,d,t is_collinear & b9,d9,t is_collinear & c,d,u is_collinear & o <> a9 & d <> d9 & o <> b9 holds
not s,t,u is_collinear
let a, b, c, o, d, d9, a9, b9, s, t, u be Element of FCPS; ::_thesis: ( a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & a,d,s is_collinear & a9,d9,s is_collinear & b,d,t is_collinear & b9,d9,t is_collinear & c,d,u is_collinear & o <> a9 & d <> d9 & o <> b9 implies not s,t,u is_collinear )
assume that
A1: a,b,c,o are_coplanar and
A2: not a,b,c,d are_coplanar and
A3: not a,b,d,o are_coplanar and
A4: o,d,d9 is_collinear and
A5: o,a,a9 is_collinear and
A6: o,b,b9 is_collinear and
A7: a,d,s is_collinear and
A8: a9,d9,s is_collinear and
A9: b,d,t is_collinear and
A10: b9,d9,t is_collinear and
A11: c,d,u is_collinear and
A12: o <> a9 and
A13: d <> d9 and
A14: o <> b9 ; ::_thesis: not s,t,u is_collinear
A15: d,b,c,b are_coplanar by Th14;
A16: not d,b,c,a are_coplanar by A2, Th7;
then A17: not d,b,c is_collinear by Th6;
 not b,d,o is_collinear by A3, Th6;
then  not o,b,d is_collinear by Th1;
then A18: t <> d by A4, A6, A10, A13, A14, Th5;
 ( d,b,t is_collinear & d,c,u is_collinear ) by A9, A11, Th1;
then A19: t <> u by A17, A18, Lm1;
A20: d,b,c,d are_coplanar by Th14;
 not d,o,a is_collinear by A3, Th6;
then  not o,a,d is_collinear by Th1;
then  s <> d by A4, A5, A8, A12, A13, Th5;
then A21: not d,b,c,s are_coplanar by A7, A16, Th15;
 b <> d by A2, Th14;
then A22: d,b,c,t are_coplanar by A9, A15, A20, Th10;
 d,b,c,c are_coplanar by Th14;
then  d,b,c,u are_coplanar by A1, A3, A11, A20, Th10;
then  not t,u,s is_collinear by A21, A22, A19, Th10;
hence  not s,t,u is_collinear by Th1; ::_thesis: verum
end;

definition
let FCPS be up-3-dimensional CollProjectiveSpace;
let o, a, b, c be Element of FCPS;
predo,a,b,c constitute_a_quadrangle  means :Def2: :: PROJDES1:def 2
( not a,b,c is_collinear & not o,a,b is_collinear & not o,b,c is_collinear & not o,c,a is_collinear );
end;

:: deftheorem Def2 defines constitute_a_quadrangle PROJDES1:def_2_:_
 for FCPS being up-3-dimensional CollProjectiveSpace
for o, a, b, c being Element of FCPS holds
( o,a,b,c constitute_a_quadrangle iff ( not a,b,c is_collinear & not o,a,b is_collinear & not o,b,c is_collinear & not o,c,a is_collinear ) );

Lm7:  for FCPS being up-3-dimensional CollProjectiveSpace
for o, a9, b9, c9, a, b, c, p, q, r being Element of FCPS st o <> a9 & o <> b9 & o <> c9 & a <> a9 & b <> b9 & o,a,b,c constitute_a_quadrangle & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds
p,q,r is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for o, a9, b9, c9, a, b, c, p, q, r being Element of FCPS st o <> a9 & o <> b9 & o <> c9 & a <> a9 & b <> b9 & o,a,b,c constitute_a_quadrangle & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear holds
p,q,r is_collinear
let o, a9, b9, c9, a, b, c, p, q, r be Element of FCPS; ::_thesis: ( o <> a9 & o <> b9 & o <> c9 & a <> a9 & b <> b9 & o,a,b,c constitute_a_quadrangle & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,q is_collinear & b9,c9,q is_collinear & a,c,r is_collinear & a9,c9,r is_collinear implies p,q,r is_collinear )
assume that
A1: o <> a9 and
A2: o <> b9 and
A3: o <> c9 and
A4: a <> a9 and
A5: b <> b9 and
A6: o,a,b,c constitute_a_quadrangle and
A7: o,a,a9 is_collinear and
A8: o,b,b9 is_collinear and
A9: o,c,c9 is_collinear and
A10: a,b,p is_collinear and
A11: a9,b9,p is_collinear and
A12: b,c,q is_collinear and
A13: b9,c9,q is_collinear and
A14: a,c,r is_collinear and
A15: a9,c9,r is_collinear ; ::_thesis: p,q,r is_collinear
A16: not o,b,c is_collinear by A6, Def2;
A17: not a,b,c is_collinear by A6, Def2;
A18: not o,c,a is_collinear by A6, Def2;
A19: not o,a,b is_collinear by A6, Def2;
A20: now__::_thesis:_(_a,b,c,o_are_coplanar_implies_p,q,r_is_collinear_)
assume A21: a,b,c,o are_coplanar ; ::_thesis: p,q,r is_collinear
then A22: b,c,a,o are_coplanar by Th7;
A23: a,c,b,o are_coplanar by A21, Th7;
consider d being Element of FCPS such that
A24: not a,b,c,d are_coplanar by A17, Th13;
A25: not a,c,b,d are_coplanar by A24, Th7;
A26: a,b,c,c are_coplanar by Th14;
A27: not b,c,a,d are_coplanar by A24, Th7;
consider d9 being Element of FCPS such that
A28: o <> d9 and
A29: d <> d9 and
A30: o,d,d9 is_collinear by ANPROJ_2:def_10;
 a,o,a9 is_collinear by A7, Th1;
then consider s being Element of FCPS such that
A31: a,d,s is_collinear and
A32: a9,d9,s is_collinear by A30, ANPROJ_2:def_9;
A33: d,a,s is_collinear by A31, Th1;
 b,o,b9 is_collinear by A8, Th1;
then consider t being Element of FCPS such that
A34: ( b,d,t is_collinear & b9,d9,t is_collinear ) by A30, ANPROJ_2:def_9;
 c,o,c9 is_collinear by A9, Th1;
then consider u being Element of FCPS such that
A35: c,d,u is_collinear and
A36: c9,d9,u is_collinear by A30, ANPROJ_2:def_9;
A37: s,t,u,s are_coplanar by Th14;
 not a,c,o is_collinear by A18, Th1;
then A38: not a,c,d,o are_coplanar by A25, A23, Th18;
then  not a9,c9,d9 is_collinear by A1, A3, A7, A9, A28, A30, Th19;
then  r,u,s is_collinear by A4, A7, A14, A15, A31, A32, A35, A36, A38, Th17;
then A39: s,u,r is_collinear by Th1;
 not a,b,o is_collinear by A19, Th1;
then A40: not a,b,d,o are_coplanar by A21, A24, Th18;
then  not d,o,a is_collinear by Th6;
then A41: not o,d,a is_collinear by Th1;
A42: s,t,u,u are_coplanar by Th14;
 not b,c,o is_collinear by A16, Th1;
then A43: not b,c,d,o are_coplanar by A27, A22, Th18;
then  not b9,c9,d9 is_collinear by A2, A3, A8, A9, A28, A30, Th19;
then  q,u,t is_collinear by A5, A8, A12, A13, A34, A35, A36, A43, Th17;
then A44: u,t,q is_collinear by Th1;
A45: s,t,u,t are_coplanar by Th14;
 d9,a9,s is_collinear by A32, Th1;
then  s <> a by A4, A7, A28, A30, A41, Th5;
then A46: not a,b,c,s are_coplanar by A24, A33, Th15;
A47: a,b,c,b are_coplanar by Th14;
 not a9,b9,d9 is_collinear by A1, A2, A7, A8, A28, A30, A40, Th19;
then  p,t,s is_collinear by A4, A7, A10, A11, A31, A32, A34, A40, Th17;
then A48: t,s,p is_collinear by Th1;
A49: a,b,c,a are_coplanar by Th14;
A50: not s,t,u is_collinear by A1, A2, A7, A8, A21, A24, A29, A30, A31, A32, A34, A35, A40, Th20;
then  t <> u by ANPROJ_2:def_7;
then A51: s,t,u,q are_coplanar by A44, A45, A42, Th10;
 c <> a by A18, ANPROJ_2:def_7;
then A52: a,b,c,r are_coplanar by A14, A49, A26, Th10;
 b <> c by A16, ANPROJ_2:def_7;
then A53: a,b,c,q are_coplanar by A12, A47, A26, Th10;
 a <> b by A19, ANPROJ_2:def_7;
then A54: a,b,c,p are_coplanar by A10, A49, A47, Th10;
 u <> s by A50, ANPROJ_2:def_7;
then A55: s,t,u,r are_coplanar by A39, A37, A42, Th10;
 s <> t by A50, ANPROJ_2:def_7;
then  s,t,u,p are_coplanar by A48, A37, A45, Th10;
hence  p,q,r is_collinear by A17, A50, A46, A54, A53, A52, A51, A55, Th16; ::_thesis: verum
end;
now__::_thesis:_(_not_a,b,c,o_are_coplanar_implies_p,q,r_is_collinear_)
assume A56: not a,b,c,o are_coplanar ; ::_thesis: p,q,r is_collinear
then  not a9,b9,c9 is_collinear by A1, A2, A3, A7, A8, A9, Th19;
hence  p,q,r is_collinear by A4, A7, A10, A11, A12, A13, A14, A15, A56, Th17; ::_thesis: verum
end;
hence  p,q,r is_collinear by A20; ::_thesis: verum
end;

theorem Th21: :: PROJDES1:21
for FCPS being up-3-dimensional CollProjectiveSpace
for o, a, b, c, a9, b9, c9, p, r, q being Element of FCPS st not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & a <> a9 & b,c,r is_collinear & b9,c9,r is_collinear & a,c,q is_collinear & b <> b9 & a9,c9,q is_collinear & o <> a9 & o <> b9 & o <> c9 holds
r,q,p is_collinear
proof
let FCPS be up-3-dimensional CollProjectiveSpace; ::_thesis: for o, a, b, c, a9, b9, c9, p, r, q being Element of FCPS st not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & a <> a9 & b,c,r is_collinear & b9,c9,r is_collinear & a,c,q is_collinear & b <> b9 & a9,c9,q is_collinear & o <> a9 & o <> b9 & o <> c9 holds
r,q,p is_collinear
let o, a, b, c, a9, b9, c9, p, r, q be Element of FCPS; ::_thesis: ( not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & a <> a9 & b,c,r is_collinear & b9,c9,r is_collinear & a,c,q is_collinear & b <> b9 & a9,c9,q is_collinear & o <> a9 & o <> b9 & o <> c9 implies r,q,p is_collinear )
assume that
A1: not o,a,b is_collinear and
A2: not o,b,c is_collinear and
A3: not o,a,c is_collinear and
A4: ( o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear ) and
A5: a,b,p is_collinear and
A6: ( a9,b9,p is_collinear & a <> a9 ) and
A7: b,c,r is_collinear and
A8: b9,c9,r is_collinear and
A9: a,c,q is_collinear and
A10: ( b <> b9 & a9,c9,q is_collinear & o <> a9 & o <> b9 & o <> c9 ) ; ::_thesis: r,q,p is_collinear
A11: now__::_thesis:_(_a,b,c_is_collinear_implies_r,q,p_is_collinear_)
A12: ( b <> c & b,c,b is_collinear ) by A2, ANPROJ_2:def_7;
assume A13: a,b,c is_collinear ; ::_thesis: r,q,p is_collinear
then  b,c,a is_collinear by Th1;
then A14: a,b,r is_collinear by A7, A12, ANPROJ_2:def_8;
A15: ( c <> a & a,c,a is_collinear ) by A3, ANPROJ_2:def_7;
 a,c,b is_collinear by A13, Th1;
then A16: a,b,q is_collinear by A9, A15, ANPROJ_2:def_8;
 a <> b by A1, ANPROJ_2:def_7;
hence  r,q,p is_collinear by A5, A14, A16, ANPROJ_2:def_8; ::_thesis: verum
end;
A17: not o,c,a is_collinear by A3, Th1;
now__::_thesis:_(_not_a,b,c_is_collinear_implies_r,q,p_is_collinear_)
assume  not a,b,c is_collinear ; ::_thesis: r,q,p is_collinear
then  o,a,b,c constitute_a_quadrangle by A1, A2, A17, Def2;
then  p,r,q is_collinear by A4, A5, A6, A7, A8, A9, A10, Lm7;
hence  r,q,p is_collinear by Th1; ::_thesis: verum
end;
hence  r,q,p is_collinear by A11; ::_thesis: verum
end;

theorem Th22: :: PROJDES1:22
for CS being up-3-dimensional CollProjectiveSpace holds CS is Desarguesian
proof
let CS be up-3-dimensional CollProjectiveSpace; ::_thesis: CS is Desarguesian
 for o, a, b, c, a9, b9, c9, r, q, p being Element of CS st o <> a9 & a <> a9 & o <> b9 & b <> b9 & o <> c9 & c <> c9 & not o,a,b is_collinear & not o,a,c is_collinear & not o,b,c is_collinear & a,b,p is_collinear & a9,b9,p is_collinear & b,c,r is_collinear & b9,c9,r is_collinear & a,c,q is_collinear & a9,c9,q is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear & o,c,c9 is_collinear holds
r,q,p is_collinear by Th21;
hence  CS is Desarguesian by ANPROJ_2:def_12; ::_thesis: verum
end;

registration
clusterV38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional  ->  Desarguesian up-3-dimensional for L13();
correctness
coherence
for b1 being up-3-dimensional CollProjectiveSpace holds b1 is Desarguesian ;
by Th22;
end;