:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation :: by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and :: Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies AFVECT0, SUBSET_1, XBOOLE_0, RELAT_1, ZFMISC_1, ANALOAF, PARSP_1, DIRAF, STRUCT_0, AFVECT01; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFVECT0, RELSET_1; constructors DOMAIN_1, DIRAF, AFVECT0; registrations XBOOLE_0, STRUCT_0, AFVECT0; requirements SUBSET, BOOLE; begin reserve AFV for WeakAffVect; reserve a,a9,b,b9,c,d,p,p9,q,q9,r,r9 for Element of AFV; registration 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; attr IT is WeakAffSegm-like means :: AFVECT01:def 1 (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 IT st a,b // b,c) & (for a,a9,b, b9,p being Element of IT st a<>a9 & b<>b9& p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9) & (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,p9 being Element of IT st (p<>p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b)) & (for a,b,b9,p,p9,c being Element of IT st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c) & (for a,b,b9,c being Element of IT st a<>c & b<>b9 & a,b // b,c & a,b9 // b9,c holds ex p,p9 being Element of IT st p<>p9 & b,b9 // p,p9& b,p // p,b9 & b,p9 // p9, b9) & for a,b,c,p,p9,q,q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a, p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r,r9 being Element of IT st b,c // r,r9 & b,r // r,c & b,r9 // r9,c; end; registration cluster strict WeakAffSegm-like for non trivial AffinStruct; end; definition mode WeakAffSegm is WeakAffSegm-like non trivial AffinStruct; end; :: :: PROPERTIES OF RELATION OF CONGRUENCE OF THE CARRIER :: reserve AFV for WeakAffSegm; reserve a,b,b9,b99,c,d,p,p9 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,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b implies a=c; theorem :: AFVECT01:8 a,b9 // a,b99 & a,b // a,b99 implies b=b9 or b=b99 or b9=b99; :: :: RELATION OF MAXIMAL DISTANCE AND MIDPOINT RELATION :: definition let AFV; let a,b; pred MDist a,b means :: AFVECT01:def 2 ex p,p9 st p<>p9 & a,b // p,p9 & a,p // p,b & a, p9 // p9,b; end; definition let AFV; let a,b,c; pred Mid a,b,c means :: AFVECT01:def 3 a=b & b=c & a=c or a=c & MDist a,b or a<>c & a,b // b,c; end; theorem :: AFVECT01:9 a<>b & not MDist a,b implies ex c st a<>c & a,b // b,c; theorem :: AFVECT01:10 MDist a,b & a,b // b,c implies a=c; theorem :: AFVECT01:11 MDist a,b implies a<>b;