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

### Classical and Non-classical Pasch Configurations in Ordered Affine Planes

by
Henryk Oryszczyszyn,
Krzysztof Prazmowski, and
Malgorzata Prazmowska

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