Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

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

**by****Jolanta Swierzynska, and****Bogdan Swierzynski**- Received October 31, 1990
- 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;

Back to top