The abstract of the Mizar article:

Metric-Affine Configurations in Metric Affine Planes --- Part I

by

Jolanta Swierzynska, and

Bogdan Swierzynski

Received October 31, 1990

MML identifier: CONAFFM

[ Mizar article, MML identifier index ]

environ

 vocabulary ANALMETR, DIRAF, ANALOAF, SYMSP_1, CONAFFM;
 notation SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR;
 constructors AFF_1, ANALMETR, XBOOLE_0;
 clusters ANALMETR, ZFMISC_1, XBOOLE_0;


begin

 reserve X for OrtAfPl;
 reserve o,a,a1,a2,b,b1,b2,c,c1,c2,d,e1,e2
        for Element of X;
 reserve b2',c2',d1'
        for Element of Af(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;
  synonym DES_holds_in X;

  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;
  synonym AH_holds_in X;

  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);
  synonym 3H_holds_in X;

  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;
  synonym ODES_holds_in X;

  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;
  synonym LIN_holds_in X;

  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;
  synonym LIN1_holds_in X;

  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;
  synonym LIN2_holds_in X;
end;

theorem :: CONAFFM:1
ODES_holds_in X implies DES_holds_in X;

theorem :: CONAFFM:2
ODES_holds_in X implies AH_holds_in X;

theorem :: CONAFFM:3
LIN_holds_in X implies LIN1_holds_in X;

 theorem :: CONAFFM:4
LIN1_holds_in X implies LIN2_holds_in X;

theorem :: CONAFFM:5
LIN_holds_in X implies ODES_holds_in X;

theorem :: CONAFFM:6
LIN_holds_in X implies 3H_holds_in X;