The abstract of the Mizar article:

Desargues Theorem In Projective 3-Space

by

Eugeniusz Kusak

Received August 13, 1990

MML identifier: PROJDES1

[ Mizar article, MML identifier index ]

environ

 vocabulary ANPROJ_2, INCSP_1, AFF_2, PROJDES1;
 notation STRUCT_0, COLLSP, ANPROJ_2;
 constructors ANPROJ_2, XBOOLE_0;
 clusters ANPROJ_2, ZFMISC_1, XBOOLE_0;


begin

 reserve FCPS for up-3-dimensional CollProjectiveSpace;
 reserve a,a',b,b',c,c',d,d',o,p,q,r,s,t,u,x,y,z
         for Element of FCPS;

theorem :: PROJDES1:1
 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;

canceled 3;

theorem :: PROJDES1:5
   ex q,r st not p,q,r is_collinear;

theorem :: PROJDES1:6
   not a,b,c is_collinear & a,b,b' is_collinear & a<>b' implies
      not a,b',c is_collinear;

theorem :: PROJDES1:7
   not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear
      implies a=d;

theorem :: PROJDES1:8
 not o,a,d is_collinear & o,d,d' is_collinear & a,d,s is_collinear &
d<>d' & a',d',s is_collinear & o,a,a' is_collinear & o<>a' implies s<>d;

definition let FCPS,a,b,c,d;
 pred a,b,c,d are_coplanar means
:: PROJDES1:def 1
  ex x being Element of FCPS
 st a,b,x is_collinear & c,d,x is_collinear;
end;

canceled;

theorem :: PROJDES1:10
 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;

theorem :: PROJDES1:11
 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;

theorem :: PROJDES1:12
 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;

theorem :: PROJDES1:13
   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
;

theorem :: PROJDES1:14
 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;

theorem :: PROJDES1:15
   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 st p,q,x is_collinear
& r,s,x is_collinear;

theorem :: PROJDES1:16
 ex a,b,c,d st not a,b,c,d are_coplanar;

theorem :: PROJDES1:17
 not p,q,r is_collinear implies ex s st not p,q,r,s are_coplanar;

theorem :: PROJDES1:18
 a=b or a=c or b=c or a=d or b=d or d=c implies a,b,c,d are_coplanar;

theorem :: PROJDES1:19
 not a,b,c,o are_coplanar & o,a,a' is_collinear & a<>a' implies not
       a,b,c,a' are_coplanar;

theorem :: PROJDES1:20
 not a,b,c is_collinear & 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',p are_coplanar & a',b',c',q are_coplanar & a',b',c',r are_coplanar &
not a,b,c,a' are_coplanar implies p,q,r is_collinear;

theorem :: PROJDES1:21
 a<>a' & o,a,a' is_collinear & not a,b,c,o are_coplanar & not
a',b',c' is_collinear & a,b,p is_collinear & a',b',p is_collinear &
b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear &
a',c',r is_collinear implies p,q,r is_collinear;

theorem :: PROJDES1:22
 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;

theorem :: PROJDES1:23
 not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear
       & o,c,c' is_collinear & o<>a' & o<>b' & o<>c' implies
     not a',b',c' is_collinear & not a',b',c',o are_coplanar;

theorem :: PROJDES1:24
 a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not
     a,b,d,o are_coplanar & not b,c,d,o are_coplanar & not a,c,d,o are_coplanar
& o,d,d' is_collinear & o,a,a' is_collinear & o,b,b' is_collinear &
o,c,c' is_collinear & a,d,s is_collinear & a',d',s is_collinear &
b,d,t is_collinear & b',d',t is_collinear & c,d,u is_collinear & o<>a' & o<>d'
& d<>d' & o<>b' implies not s,t,u is_collinear;

definition let FCPS,o,a,b,c;
pred o,a,b,c constitute_a_quadrangle means
:: 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;

canceled;

theorem :: PROJDES1:26
 not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear
     & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear &
     a,b,p is_collinear & a',b',p is_collinear & a<>a' & b,c,r is_collinear &
     b',c',r is_collinear & a,c,q is_collinear & b<>b' & a',c',q is_collinear &
     o<>a' & o<>b' & o<>c' implies r,q,p is_collinear;

theorem :: PROJDES1:27
for CS being up-3-dimensional CollProjectiveSpace holds
                   CS is Desarguesian;

definition
 cluster -> Desarguesian (up-3-dimensional CollProjectiveSpace);
end;