The abstract of the Mizar article:

One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation

by

Barbara Konstanta,

Urszula Kowieska,

Grzegorz Lewandowski, and

Krzysztof Prazmowski

Received October 4, 1990

MML identifier: AFVECT01

[ Mizar article, MML identifier index ]

environ

 vocabulary AFVECT0, RELAT_1, ANALOAF, PARSP_1, DIRAF, REALSET1, AFVECT01;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ANALOAF, DIRAF,
      AFVECT0, RELSET_1, REALSET1;
 constructors AFVECT0, DIRAF, DOMAIN_1, MEMBERED, XBOOLE_0;
 clusters AFVECT0, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve AFV for WeakAffVect;
reserve a,a',b,b',c,d,p,p',q,q',r,r' for Element of AFV;

definition
 let A be non empty set, C be Relation of [:A,A:];
 cluster AffinStruct(#A,C#) -> non empty;
end;

definition let IT be non empty AffinStruct;
 canceled;

  attr IT is WeakAffSegm-like means
:: AFVECT01:def 2
(for a,b being Element of IT holds a,b // b,a) &
(for a,b being Element of IT st a,b // a,a holds a=b) &
(for a,b,c,d,p,q being Element of IT st a,b // p,q &
  c,d // p,q holds a,b // c,d) &
(for a,c being Element of IT ex b being Element of the carrier
 of IT st a,b // b,c) &
(for a,a',b,b',p being Element of IT st a<>a' & b<>b'&
 p,a // p,a' & p,b // p,b' holds a,b // a',b') &
(for a,b being Element of IT holds a=b or
 ex c being Element of IT st ( a<>c & a,b // b,c) or
 ex p,p' being Element of IT st
             (p<>p' & a,b // p,p' & a,p // p,b & a,p' // p',b)) &
(for a,b,b',p,p',c being Element of IT st a,b // b,c &
 b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds a,b' // b',c) &
(for a,b,b',c being Element of IT st a<>c & b<>b' & a,b // b,c &
 a,b' // b',c holds ex p,p' being Element of IT st
 p<>p' & b,b' // p,p'& b,p // p,b' & b,p' // p',b') &
(for a,b,c,p,p',q,q' being Element of IT st
 (a,b // p,p' & a,c // q,q' & a,p // p,b &
  a,q // q,c & a,p' // p',b & a,q' // q',c) holds ex
  r,r' being Element of IT st
    b,c // r,r' & b,r // r,c & b,r' // r',c);
end;

definition
 cluster strict non trivial WeakAffSegm-like (non empty AffinStruct);
end;

definition
  mode WeakAffSegm is non trivial WeakAffSegm-like (non empty AffinStruct);
end;

::
::         PROPERTIES OF RELATION OF CONGRUENCE OF THE CARRIER
::

reserve AFV for WeakAffSegm;
reserve a,b,b',b'',c,d,p,p'
 for Element of AFV;

theorem :: AFVECT01:1
a,b // a,b;

theorem :: AFVECT01:2
a,b // c,d implies c,d // a,b;

theorem :: AFVECT01:3
a,b // c,d implies a,b // d,c;

theorem :: AFVECT01:4
a,b // c,d implies b,a // c,d;

theorem :: AFVECT01:5
for a,b holds a,a // b,b;

theorem :: AFVECT01:6
a,b // c,c implies a=b;

theorem :: AFVECT01:7
a,b // p,p' & a,b // b,c & a,p // p,b &
         a,p' // p',b implies a=c;

theorem :: AFVECT01:8
a,b' // a,b'' & a,b // a,b''
        implies b=b' or b=b'' or b'=b'';

::
::          RELATION OF MAXIMAL DISTANCE AND MIDPOINT RELATION
::

definition let AFV;let a,b; canceled;

pred MDist a,b means
:: AFVECT01:def 4
  ex p,p' st p<>p' & a,b // p,p' & a,p // p,b & a,p' // p',b;
 end;

definition let AFV; let a,b,c;
  pred Mid a,b,c means
:: AFVECT01:def 5
    (a=b & b=c & a=c) or (a=c & MDist a,b) or (a<>c & a,b // b,c);
end;

canceled 2;

theorem :: AFVECT01:11
a<>b & not MDist a,b implies ex c st ( a<>c & a,b // b,c );

theorem :: AFVECT01:12
MDist a,b & a,b // b,c implies a=c;

theorem :: AFVECT01:13
MDist a,b implies a<>b;