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

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

by
Barbara Konstanta,
Urszula Kowieska,
Grzegorz Lewandowski, and
Krzysztof Prazmowski

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