Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### 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;

```