:: Classical and Non--classical Pasch Configurations in Ordered Affine Planes :: by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and :: Ma{\l}gorzata Pra\.zmowska :: :: Received May 16, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ANALOAF, SUBSET_1, DIRAF, PARSP_1, VECTSP_1, PASCH, PENCIL_1; notations STRUCT_0, ANALOAF, DIRAF; constructors DIRAF; registrations STRUCT_0; begin reserve OAS for OAffinSpace; reserve a,a9,b,b9,c,c9,d,d1,d2,e1,e2,e3,e4,e5,e6,p,p9,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 p,b,c are_collinear & Mid b,p,a & p,c,d are_collinear & b,c '||' d,a holds Mid c,p,d; 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 & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds Mid p,a,d; end; definition let OAS; attr OAS is satisfying_Gen_Par_Pasch means :: PASCH:def 3 for a,b,c,a9,b9,c9 st not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds Mid a9,b9,c9; 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 a,b,c are_collinear holds ex y st Mid a,y,c & Mid y,x,d; 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 a,b,c are_collinear holds ex y st Mid b,y,c & Mid x,y,d; 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 a,b,c are_collinear ex x st Mid a,x,d & Mid b,x,c; end; theorem :: PASCH:1 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:2 p,b // p,c & p<>c & b<>p implies ex d st p,a // p,d & a,b '||' c, d & c <>d; theorem :: PASCH:3 p,b '||' p,c & p<>b implies ex d st p,a '||' p,d & a,b '||' c,d; theorem :: PASCH:4 not p,a,b are_collinear & p,b,c are_collinear & p,a,d1 are_collinear & p,a,d2 are_collinear & a,b '||' c,d1 & a,b '||' c,d2 implies d1=d2; theorem :: PASCH:5 not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 implies d1=d2; theorem :: PASCH:6 not p,b,c are_collinear & Mid b,p,a & p,c,d are_collinear & b,c '||' d,a implies Mid c,p,d; theorem :: PASCH:7 OAS is satisfying_Int_Par_Pasch; theorem :: PASCH:8 Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear implies Mid p,a,d; theorem :: PASCH:9 OAS is satisfying_Ext_Par_Pasch; theorem :: PASCH:10 not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear implies Mid a9,b9,c9; theorem :: PASCH:11 OAS is satisfying_Gen_Par_Pasch; theorem :: PASCH:12 not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 implies a,b // b9,a9; theorem :: PASCH:13 not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 implies a,a9 // b,b9; theorem :: PASCH:14 not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c implies p,a // b,c & p,b // a,c; theorem :: PASCH:15 Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p<>c implies Mid p,d,a; theorem :: PASCH:16 Mid p,d,a & c,d // b,a & p,c // p,b & not p,a,b are_collinear & p<>c implies Mid p,c,b; theorem :: PASCH:17 not p,a,b are_collinear & p,b // p,c & b,a // c,d & p<>d implies not Mid a ,p,d; theorem :: PASCH:18 p,b // p,c & b<>p implies ex x st p,a // p,x & b,a // c,x; theorem :: PASCH:19 Mid p,c,b implies ex x st Mid p,x,a & b,a // c,x; theorem :: PASCH:20 p<>b & Mid p,b,c implies ex x st Mid p,a,x & b,a // c,x; theorem :: PASCH:21 not p,a,b are_collinear & Mid p,c,b implies ex x st Mid p,x,a & a,b // x,c; theorem :: PASCH:22 ex x st a,x // b,c & a,b // x,c; theorem :: PASCH:23 a,b // c,d & not a,b,c are_collinear implies ex x st Mid a,x,d & Mid b,x,c; theorem :: PASCH:24 OAS is Fanoian; theorem :: PASCH:25 a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear implies ex x st x,a,d are_collinear & x,b,c are_collinear; theorem :: PASCH:26 a,b '||' c,d & not a,b,c are_collinear & p,a,d are_collinear & p,b,c are_collinear implies not p,a,b are_collinear; theorem :: PASCH:27 Mid a,b,d & Mid b,x,c & not a,b,c are_collinear implies ex y st Mid a,y,c & Mid y,x,d; theorem :: PASCH:28 OAS is satisfying_Ext_Bet_Pasch; theorem :: PASCH:29 Mid a,b,d & Mid a,x,c & not a,b,c are_collinear implies ex y st Mid b,y,c & Mid x,y,d; theorem :: PASCH:30 OAS is satisfying_Int_Bet_Pasch; theorem :: PASCH:31 Mid p,a,b & p,a // p9,a9 & not p,a,p9 are_collinear & p9,a9,b9 are_collinear & p,p9 // a,a9 & p,p9 // b,b9 implies Mid p9,a9,b9;