The abstract of the Mizar article:

Hessenberg Theorem

by

Eugeniusz Kusak, and

Wojciech Leonczuk

Received October 2, 1990

MML identifier: HESSENBE

[ Mizar article, MML identifier index ]

environ

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


begin

 reserve PCPP for CollProjectiveSpace,
         a,a',a1,a2,a3,b,b',b1,b2,c,c1,c3,d,d',e,o,p,p1,p2,p3,r,q,
           q1,q2,q3,x,y for Element of PCPP;

canceled 2;

theorem :: HESSENBE:3
  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;

theorem :: HESSENBE:4
  a<>b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear;

theorem :: HESSENBE:5
    p<>q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear
     implies a,b,r is_collinear;

theorem :: HESSENBE:6
  p<>q implies ex r st not p,q,r is_collinear;

theorem :: HESSENBE:7
    ex q,r st not p,q,r is_collinear;

theorem :: HESSENBE:8
  not a,b,c is_collinear & a,b,b' is_collinear & a<>b' implies
      not a,b',c is_collinear;

theorem :: HESSENBE:9
 not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear
      implies a=d;

theorem :: HESSENBE:10
 not o,a,d is_collinear & o,d,d' is_collinear & a,d,x is_collinear &
     d<>d' & a',d',x is_collinear & o,a,a' is_collinear & o<>a' implies x<>d;

canceled;

theorem :: HESSENBE:12
 not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear &
    a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear &
     c3<>a1 & c3<>a2 & c1<>a2 & c1<>a3 implies a1<>x & a3<>x;

theorem :: HESSENBE:13
 not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear &
       e<>c & d<>a implies not e,a,c is_collinear;

theorem :: HESSENBE:14
 not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear &
      q1,q2,q3 is_collinear & p1<>q2 & q2<>q3 implies not p2,p1,q3 is_collinear
;

theorem :: HESSENBE:15
   not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear &
  p3<>q2 & p2<>p3 implies not p3,p2,q2 is_collinear;

theorem :: HESSENBE:16
 not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear &
    q1,q2,p1 is_collinear & p1<>p3 & p1<>q2 implies not p3,p1,q2 is_collinear;

theorem :: HESSENBE:17
 a1<>a2 & b1<>b2 & b1,b2,x is_collinear & b1,b2,y is_collinear &
a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear
implies x=y;

canceled;

theorem :: HESSENBE:19
 not o,a1,a2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear
 & o<>b1 & o<>b2 implies not o,b1,b2 is_collinear;

reserve PCPP for Pappian CollProjectivePlane,
        a,a1,a2,a3,b1,b2,b3,c1,c2,c3,o,p,p1,p2,p3,q,q',
        q1,q2,q3,r,r1,r2,r3,x,y,z for Element of PCPP;

theorem :: HESSENBE:20
  p2<>p3 & p1<>p3 & q2<>q3 & q1<>q2 & q1<>q3 &
  not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear &
  p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear &
  p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear
                                              implies r1,r2,r3 is_collinear;

theorem :: HESSENBE:21
 o<>b1 & a1<>b1 & o<>b2 & a2<>b2 & o<>b3 & a3<>b3 & not o,a1,a2 is_collinear &
 not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear &
 b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear &
 a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear &
 o,a2,b2 is_collinear & o,a3,b3 is_collinear implies c1,c2,c3 is_collinear;

definition
 cluster Pappian -> Desarguesian CollProjectiveSpace;
end;