:: Metric-Affine Configurations in Metric Affine Planes - Part I :: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski :: :: Received October 31, 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 ANALMETR, SUBSET_1, DIRAF, ANALOAF, SYMSP_1, CONAFFM; notations STRUCT_0, ANALOAF, AFF_1, ANALMETR; constructors AFF_1, ANALMETR; registrations ANALMETR; begin reserve X for OrtAfPl; reserve o,a,a1,a2,b,b1,b2,c,c1,c2,d,e1,e2 for Element of X; reserve b29,c29,d19 for Element of the AffinStruct of X; definition let X; attr X is satisfying_DES means :: CONAFFM:def 1 for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1; attr X is satisfying_AH means :: CONAFFM:def 2 for o,a,a1,b,b1,c,c1 st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1; attr X is satisfying_3H means :: CONAFFM:def 3 for a,b,c st not LIN a,b,c holds ex d st d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b; attr X is satisfying_ODES means :: CONAFFM:def 4 for o,a,a1,b,b1,c,c1 st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1; attr X is satisfying_LIN means :: CONAFFM:def 5 for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & a<>b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds a,a1 // b,b1; attr X is satisfying_LIN1 means :: CONAFFM:def 6 for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & a<>b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1 holds b,c _|_ b1,c1; attr X is satisfying_LIN2 means :: CONAFFM:def 7 for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & a<>b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds o,c _|_ o,c1; end; theorem :: CONAFFM:1 X is satisfying_ODES implies X is satisfying_DES; theorem :: CONAFFM:2 X is satisfying_ODES implies X is satisfying_AH; theorem :: CONAFFM:3 X is satisfying_LIN implies X is satisfying_LIN1; theorem :: CONAFFM:4 X is satisfying_LIN1 implies X is satisfying_LIN2; theorem :: CONAFFM:5 X is satisfying_LIN implies X is satisfying_ODES; theorem :: CONAFFM:6 X is satisfying_LIN implies X is satisfying_3H;