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

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

by
Jolanta Swierzynska, and
Bogdan Swierzynski

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