begin
theorem Th1:
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 )
theorem Th5:
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
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
::
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:
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
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
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
theorem Th7:
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 )
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
theorem Th8:
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
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
theorem
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
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
theorem Th10:
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
theorem
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 )
theorem Th15:
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
theorem Th16:
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
theorem Th17:
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
theorem Th18:
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
theorem Th19:
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 )
theorem Th20:
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
definition
let FCPS be
up-3-dimensional CollProjectiveSpace;
let o,
a,
b,
c be
Element of
FCPS;
pred o,
a,
b,
c constitute_a_quadrangle means :
Def2:
( 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
theorem Th21:
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