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;