The abstract of the Mizar article:

The Collinearity Structure

by

Wojciech Skaba

Received May 9, 1990

MML identifier: COLLSP

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, PRE_TOPC, INCSP_1, RELAT_2, COLLSP;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, DOMAIN_1, STRUCT_0,
      PRE_TOPC;
 constructors REAL_1, DOMAIN_1, STRUCT_0, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE;


begin :: AUXILIARY THEOREMS

 reserve X for set;

definition let X;
  mode Relation3 of X -> set means
:: COLLSP:def 1
it c= [:X,X,X:];
end;

canceled;

theorem :: COLLSP:2
      X = {}
      or ex a be set st {a} = X
      or ex a,b be set st a<>b & a in X & b in X;

::                      *********************
::                      *   COLLINEARITY    *
::                      *********************

definition
  struct(1-sorted) CollStr (# carrier -> set,
                 Collinearity -> Relation3 of the carrier #);
end;

definition
 cluster non empty strict CollStr;
end;

 reserve CS for non empty CollStr;
 reserve a,b,c for Point of CS;

definition let CS, a,b,c;
  pred a,b,c is_collinear means
:: COLLSP:def 2
[a,b,c] in the Collinearity of CS;
end;

definition let IT be non empty CollStr;
  attr IT is reflexive means
:: COLLSP:def 3

    for a,b,c being Point of IT
       st a=b or a=c or b=c holds [a,b,c] in the Collinearity of IT;
end;

definition let IT be non empty CollStr;
  attr IT is transitive means
:: COLLSP:def 4

   for a,b,p,q,r being Point of IT
     st a<>b & [a,b,p] in the Collinearity of IT &
                [a,b,q] in the Collinearity of IT &
                [a,b,r] in the Collinearity of IT
      holds [p,q,r] in the Collinearity of IT;
end;

definition
 cluster strict reflexive transitive (non empty CollStr);
end;

definition
  mode CollSp is reflexive transitive (non empty CollStr);
end;

 reserve CLSP for CollSp;
 reserve a,b,c,d,p,q,r for Point of CLSP;

canceled 4;

theorem :: COLLSP:7
 (a=b or a=c or b=c) implies a,b,c is_collinear;

theorem :: COLLSP:8
 a<>b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear
      implies p,q,r is_collinear;

theorem :: COLLSP:9
 a,b,c is_collinear implies b,a,c is_collinear & a,c,b is_collinear;

theorem :: COLLSP:10
   a,b,a is_collinear;

theorem :: COLLSP:11
 a<>b & a,b,c is_collinear & a,b,d is_collinear
       implies a,c,d is_collinear;

theorem :: COLLSP:12
   a,b,c is_collinear implies b,a,c is_collinear;

theorem :: COLLSP:13
  a,b,c is_collinear implies b,c,a is_collinear;

theorem :: COLLSP:14
 p<>q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear
      implies a,b,r is_collinear;

::                      *******************
::                      *      LINES      *
::                      *******************

definition let CLSP,a,b;
  func Line(a,b) -> set equals
:: COLLSP:def 5
    {p: a,b,p is_collinear};
end;

canceled;

theorem :: COLLSP:16
  a in Line(a,b) & b in Line(a,b);

theorem :: COLLSP:17
   a,b,r is_collinear iff r in Line(a,b);

::                ************************************
::                *    PROPER COLLINEARITY SPACES    *
::                ************************************

 reserve i,j,k for Nat;

definition let IT be non empty CollStr;
  attr IT is proper means
:: COLLSP:def 6
   ex a,b,c being Point of IT st not a,b,c is_collinear;
end;

definition
 cluster strict proper CollSp;
end;

 reserve CLSP for proper CollSp;
 reserve a,b,c,d,p,q,r for Point of CLSP;

canceled;

theorem :: COLLSP:19
  for p,q holds p<>q implies ex r st not p,q,r is_collinear;

definition let CLSP;
  mode LINE of CLSP -> set means
:: COLLSP:def 7
   ex a,b st a<>b & it=Line(a,b);
end;

 reserve P,Q for LINE of CLSP;

canceled 2;

theorem :: COLLSP:22
    a=b implies Line(a,b) = the carrier of CLSP;

theorem :: COLLSP:23
    for P ex a,b st a<>b & a in P & b in P;

theorem :: COLLSP:24
    a <> b implies ex P st a in P & b in P;

 theorem :: COLLSP:25
   p in P & q in P & r in P implies p,q,r is_collinear;

 theorem :: COLLSP:26
   P c= Q implies P = Q;

 theorem :: COLLSP:27
   p<>q & p in P & q in P implies Line(p,q) c= P;

 theorem :: COLLSP:28
   p<>q & p in P & q in P implies Line(p,q) = P;

 theorem :: COLLSP:29
   p<>q & p in P & q in P & p in Q & q in Q implies P = Q;

 theorem :: COLLSP:30
     P = Q or P misses Q or ex p st P /\ Q = {p};

theorem :: COLLSP:31
    a<>b implies Line(a,b) <> the carrier of CLSP;