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 II

by
Jolanta Swierzynska, and
Bogdan Swierzynski

MML identifier: CONMETR
[ Mizar article, MML identifier index ]

```environ

vocabulary ANALMETR, SYMSP_1, ANALOAF, AFF_1, DIRAF, INCSP_1, AFF_2, CONAFFM,
CONMETR;
notation SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR, AFF_2, CONAFFM;
constructors AFF_1, AFF_2, CONAFFM, XBOOLE_0;
clusters ANALMETR, ZFMISC_1, XBOOLE_0;
requirements SUBSET;

begin

reserve X for OrtAfPl;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,c3,d,d1,d2,d3,d4,e1,e2
for Element of X;
reserve a2',a3',b2',x' for Element of Af(X);
reserve A,K,M,N for Subset of X;
reserve A',K' for Subset of Af(X);

definition let X;
attr X is satisfying_OPAP means
:: CONMETR:def 1
for o,a1,a2,a3,b1,b2,b3,M,N st o in M & a1 in M & a2 in M & a3 in M &
o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N
& o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 &
a3,b3 // a1,b1 holds a1,b2 // a2,b3;
synonym OPAP_holds_in X;

attr X is satisfying_PAP means
:: CONMETR:def 2
for o,a1,a2,a3,b1,b2,b3,M,N st M is_line & N is_line &
o in M & a1 in M & a2 in M & a3 in M &
o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N
& o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 &
a3,b3 // a1,b1 holds a1,b2 // a2,b3;
synonym PAP_holds_in X;

attr X is satisfying_MH1 means
:: CONMETR:def 3
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M &
b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M &
not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4;
synonym MH1_holds_in X;

attr X is satisfying_MH2 means
:: CONMETR:def 4
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M &
b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N &
not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 &
a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds a1,a4 _|_ b1,b4;
synonym MH2_holds_in X;

attr X is satisfying_TDES means
:: CONMETR:def 5
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 b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN
o,c,c1
& a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds a,c // a1,c1;
synonym TDES_holds_in X;

attr X is satisfying_SCH means
:: CONMETR:def 6
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line
& a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N &
b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M &
not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N &
a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
synonym SCH_holds_in X;

attr X is satisfying_OSCH means
:: CONMETR:def 7
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M & b1 in M
& b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M &
not a2 in M & not b2 in M & not b4 in M & not a1 in N &
not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 &
a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
synonym OSCH_holds_in X;

attr X is satisfying_des means
:: CONMETR:def 8
for a,a1,b,b1,c,c1 st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 &
a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1;
synonym des_holds_in X;
end;

theorem :: CONMETR:1
ex a,b,c st LIN a,b,c & a<>b & b<>c & c <>a;

theorem :: CONMETR:2
for a,b st a<>b ex c st LIN a,b,c & a<>c & b<>c;

theorem :: CONMETR:3
for A,a st A is_line ex K st a in K & A _|_ K;

theorem :: CONMETR:4
A is_line & a in A & b in A & c in A implies LIN a,b,c;

theorem :: CONMETR:5
A is_line & M is_line & a in A & b in A & a in M & b in M implies
a=b or A=M;

theorem :: CONMETR:6
for a,b,c,d,M holds for M' being Subset of Af(X),
c',d' being Element of Af(X) st c =c' & d=d' & M=M' &
a in M & b in M & c',d' // M' holds c,d // a,b;

theorem :: CONMETR:7
TDES_holds_in X implies Af(X) satisfies_TDES;

theorem :: CONMETR:8
Af(X) satisfies_des implies des_holds_in X;

theorem :: CONMETR:9
MH1_holds_in X implies OSCH_holds_in X;

theorem :: CONMETR:10
MH2_holds_in X implies OSCH_holds_in X;

theorem :: CONMETR:11
AH_holds_in X implies TDES_holds_in X;

theorem :: CONMETR:12
OSCH_holds_in X & TDES_holds_in X implies SCH_holds_in X;

theorem :: CONMETR:13
OPAP_holds_in X & DES_holds_in X implies PAP_holds_in X;

theorem :: CONMETR:14
MH1_holds_in X & MH2_holds_in X implies OPAP_holds_in X;

theorem :: CONMETR:15
3H_holds_in X implies OPAP_holds_in X;
```