The abstract of the Mizar article:

Classical and Non-classical Pasch Configurations in Ordered Affine Planes

by

Henryk Oryszczyszyn,

Krzysztof Prazmowski, and

Malgorzata Prazmowska

Received May 16, 1990

MML identifier: PASCH

[ Mizar article, MML identifier index ]

environ

 vocabulary ANALOAF, DIRAF, PARSP_1, VECTSP_1, PASCH;
 notation STRUCT_0, ANALOAF, DIRAF;
 constructors DIRAF, XBOOLE_0;
 clusters ZFMISC_1, XBOOLE_0;


begin
reserve OAS for OAffinSpace;
reserve a,a',b,b',c,c',d,d1,d2,e1,e2,e3,e4,e5,e6,p,p',q,r,x,y,z
 for Element of OAS;

definition let OAS;
 attr OAS is satisfying_Int_Par_Pasch means
:: PASCH:def 1
    for a,b,c,d,p st not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a
                                                         holds Mid c,p,d;
  synonym OAS satisfies_Int_Par_Pasch;
end;

definition let OAS;
 attr OAS is satisfying_Ext_Par_Pasch means
:: PASCH:def 2
    for a,b,c,d,p st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b
                                                        holds Mid p,a,d;
  synonym OAS satisfies_Ext_Par_Pasch;
end;

definition let OAS;
 attr OAS is satisfying_Gen_Par_Pasch means
:: PASCH:def 3
    for a,b,c,a',b',c' st
   not LIN a,b,a' & a,a' '||' b,b' & a,a' '||' c,c' & Mid a,b,c & LIN a',b',c'
                                                    holds Mid a',b',c';
  synonym OAS satisfies_Gen_Par_Pasch;
end;

definition let OAS;
 attr OAS is satisfying_Ext_Bet_Pasch means
:: PASCH:def 4
    for a,b,c,d,x,y st Mid a,b,d & Mid b,x,c & not LIN a,b,c
                             holds ex y st Mid a,y,c & Mid y,x,d;
  synonym OAS satisfies_Ext_Bet_Pasch;
end;

definition let OAS;
 attr OAS is satisfying_Int_Bet_Pasch means
:: PASCH:def 5
    for a,b,c,d,x,y st Mid a,b,d & Mid a,x,c & not LIN a,b,c
                             holds ex y st Mid b,y,c & Mid x,y,d;
  synonym OAS satisfies_Int_Bet_Pasch;
end;

definition let OAS;
 attr OAS is Fanoian means
:: PASCH:def 6
    for a,b,c,d st a,b // c,d & a,c // b,d & not LIN a,b,c
                            ex x st Mid a,x,d & Mid b,x,c;
  synonym OAS satisfies_Fano;
end;

canceled 6;

theorem :: PASCH:7
 b,p // p,c & p<>c & b<>p implies ex d st
                          a,p // p,d & a,b '||' c,d & c <>d & p<>d;

theorem :: PASCH:8
 p,b // p,c & p<>c & b<>p implies ex d st
                           p,a // p,d & a,b '||' c,d & c <>d;

theorem :: PASCH:9
   p,b '||' p,c & p<>b implies ex d st p,a '||' p,d & a,b '||' c,d;

canceled;

theorem :: PASCH:11
 not LIN p,a,b & LIN p,b,c & LIN p,a,d1 & LIN p,a,d2 &
         a,b '||' c,d1 & a,b '||' c,d2 implies d1=d2;

theorem :: PASCH:12
 not LIN a,b,c & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 &
       a,c '||' b,d2 implies d1=d2;

theorem :: PASCH:13
 not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a
                                          implies Mid c,p,d;

theorem :: PASCH:14
   OAS satisfies_Int_Par_Pasch;

theorem :: PASCH:15
 Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b
                                           implies Mid p,a,d;

theorem :: PASCH:16
   OAS satisfies_Ext_Par_Pasch;

theorem :: PASCH:17
 not LIN a,b,a' & a,a' '||' b,b' & a,a' '||' c,c' & Mid a,b,c &
                                LIN a',b',c' implies Mid a',b',c';

theorem :: PASCH:18
   OAS satisfies_Gen_Par_Pasch;

theorem :: PASCH:19
   not LIN p,a,b & a,p // p,a' & b,p // p,b' & a,b '||' a',b'
        implies a,b // b',a';

theorem :: PASCH:20
   not LIN p,a,a' & p,a // p,b & p,a' // p,b' & a,a' '||' b,b'
        implies a,a' // b,b';

theorem :: PASCH:21
 not LIN p,a,b & p,a '||' b,c & p,b '||' a,c implies
                                    p,a // b,c & p,b // a,c;

theorem :: PASCH:22
 Mid p,c,b & c,d // b,a & p,d // p,a & not LIN p,a,b & p<>c
                                              implies Mid p,d,a;

theorem :: PASCH:23
 Mid p,d,a & c,d // b,a & p,c // p,b & not LIN p,a,b & p<>c
                                              implies Mid p,c,b;

theorem :: PASCH:24
 not LIN p,a,b & p,b // p,c & b,a // c,d & LIN a,p,d & p<>d
                                           implies not Mid a,p,d;

theorem :: PASCH:25
 p,b // p,c & b<>p
                   implies ex x st p,a // p,x & b,a // c,x;

theorem :: PASCH:26
 Mid p,c,b implies ex x st Mid p,x,a & b,a // c,x;

theorem :: PASCH:27
 p<>b & Mid p,b,c implies ex x st Mid p,a,x & b,a // c,x;

theorem :: PASCH:28
 not LIN p,a,b & Mid p,c,b
                       implies ex x st Mid p,x,a & a,b // x,c;

theorem :: PASCH:29
   ex x st a,x // b,c & a,b // x,c;

theorem :: PASCH:30
 a,b // c,d & not LIN a,b,c
                     implies ex x st Mid a,x,d & Mid b,x,c;

canceled;

theorem :: PASCH:32
OAS satisfies_Fano;

theorem :: PASCH:33
   a,b '||' c,d & a,c '||' b,d & not LIN a,b,c
                           implies ex x st LIN x,a,d & LIN x,b,c;

theorem :: PASCH:34
   a,b '||' c,d & a,c '||' b,d & not LIN a,b,c & LIN p,a,d &
                                  LIN p,b,c implies not LIN p,a,b;

theorem :: PASCH:35
 Mid a,b,d & Mid b,x,c & not LIN a,b,c
                          implies ex y st Mid a,y,c & Mid y,x,d;

theorem :: PASCH:36
OAS satisfies_Ext_Bet_Pasch;

theorem :: PASCH:37
 Mid a,b,d & Mid a,x,c & not LIN a,b,c
                            implies ex y st Mid b,y,c & Mid x,y,d;

theorem :: PASCH:38
OAS satisfies_Int_Bet_Pasch;

theorem :: PASCH:39
   Mid p,a,b & p,a // p',a' & not LIN p,a,p' & LIN p',a',b' &
               p,p' // a,a' & p,p' // b,b' implies Mid p',a',b';