:: Classical and Non--classical Pasch Configurations in Ordered Affine Planes
:: by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and
::
:: Received May 16, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let OAS be OAffinSpace;
attrOAS is satisfying_Int_Par_Pasch  means :: PASCH:def 1
 for a, b, c, d, p being Element of OAS st not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a holds
Mid c,p,d;
end;

:: deftheorem  defines satisfying_Int_Par_Pasch PASCH:def_1_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_Int_Par_Pasch iff for a, b, c, d, p being Element of OAS st not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a holds
Mid c,p,d );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_Ext_Par_Pasch  means :: PASCH:def 2
 for a, b, c, d, p being Element of OAS st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b holds
Mid p,a,d;
end;

:: deftheorem  defines satisfying_Ext_Par_Pasch PASCH:def_2_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_Ext_Par_Pasch iff for a, b, c, d, p being Element of OAS st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b holds
Mid p,a,d );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_Gen_Par_Pasch  means :: PASCH:def 3
 for a, b, c, a9, b9, c9 being Element of OAS st not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds
Mid a9,b9,c9;
end;

:: deftheorem  defines satisfying_Gen_Par_Pasch PASCH:def_3_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_Gen_Par_Pasch iff for a, b, c, a9, b9, c9 being Element of OAS st not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds
Mid a9,b9,c9 );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_Ext_Bet_Pasch  means :: PASCH:def 4
 for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid b,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d );
end;

:: deftheorem  defines satisfying_Ext_Bet_Pasch PASCH:def_4_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_Ext_Bet_Pasch iff for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid b,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_Int_Bet_Pasch  means :: PASCH:def 5
 for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid a,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d );
end;

:: deftheorem  defines satisfying_Int_Bet_Pasch PASCH:def_5_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_Int_Bet_Pasch iff for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid a,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) );

definition
let OAS be OAffinSpace;
attrOAS is Fanoian  means :: PASCH:def 6
 for a, b, c, d being Element of OAS st a,b // c,d & a,c // b,d & not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c );
end;

:: deftheorem  defines Fanoian PASCH:def_6_:_
 for OAS being OAffinSpace holds
( OAS is Fanoian iff for a, b, c, d being Element of OAS st a,b // c,d & a,c // b,d & not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) );

theorem Th1: :: PASCH:1
for OAS being OAffinSpace
for b, p, c, a being Element of OAS st b,p // p,c &amp; p <> c &amp; b <> p holds
ex d being Element of OAS st
( a,p // p,d &amp; a,b '||' c,d &amp; c <> d &amp; p <> d )
proofend;

theorem Th2: :: PASCH:2
for OAS being OAffinSpace
for p, b, c, a being Element of OAS st p,b // p,c &amp; p <> c &amp; b <> p holds
ex d being Element of OAS st
( p,a // p,d &amp; a,b '||' c,d &amp; c <> d )
proofend;

theorem :: PASCH:3
for OAS being OAffinSpace
for p, b, c, a being Element of OAS st p,b '||' p,c &amp; p <> b holds
ex d being Element of OAS st
( p,a '||' p,d &amp; a,b '||' c,d )
proofend;

theorem Th4: :: PASCH:4
for OAS being OAffinSpace
for p, a, b, c, d1, d2 being Element of OAS st not LIN p,a,b &amp; LIN p,b,c &amp; LIN p,a,d1 &amp; LIN p,a,d2 &amp; a,b '||' c,d1 &amp; a,b '||' c,d2 holds
d1 = d2
proofend;

theorem Th5: :: PASCH:5
for OAS being OAffinSpace
for a, b, c, d1, d2 being Element of OAS st not LIN a,b,c &amp; a,b '||' c,d1 &amp; a,b '||' c,d2 &amp; a,c '||' b,d1 &amp; a,c '||' b,d2 holds
d1 = d2
proofend;

theorem Th6: :: PASCH:6
for OAS being OAffinSpace
for p, b, c, a, d being Element of OAS st not LIN p,b,c &amp; Mid b,p,a &amp; LIN p,c,d &amp; b,c '||' d,a holds
Mid c,p,d
proofend;

theorem :: PASCH:7
for OAS being OAffinSpace holds OAS is satisfying_Int_Par_Pasch
proofend;

theorem Th8: :: PASCH:8
for OAS being OAffinSpace
for p, b, c, a, d being Element of OAS st Mid p,b,c &amp; LIN p,a,d &amp; a,b '||' c,d &amp; not LIN p,a,b holds
Mid p,a,d
proofend;

theorem :: PASCH:9
for OAS being OAffinSpace holds OAS is satisfying_Ext_Par_Pasch
proofend;

theorem Th10: :: PASCH:10
for OAS being OAffinSpace
for a, b, a9, b9, c, c9 being Element of OAS st not LIN a,b,a9 &amp; a,a9 '||' b,b9 &amp; a,a9 '||' c,c9 &amp; Mid a,b,c &amp; LIN a9,b9,c9 holds
Mid a9,b9,c9
proofend;

theorem :: PASCH:11
for OAS being OAffinSpace holds OAS is satisfying_Gen_Par_Pasch
proofend;

theorem :: PASCH:12
for OAS being OAffinSpace
for p, a, b, a9, b9 being Element of OAS st not LIN p,a,b &amp; a,p // p,a9 &amp; b,p // p,b9 &amp; a,b '||' a9,b9 holds
a,b // b9,a9
proofend;

theorem :: PASCH:13
for OAS being OAffinSpace
for p, a, a9, b, b9 being Element of OAS st not LIN p,a,a9 &amp; p,a // p,b &amp; p,a9 // p,b9 &amp; a,a9 '||' b,b9 holds
a,a9 // b,b9
proofend;

theorem Th14: :: PASCH:14
for OAS being OAffinSpace
for p, a, b, c being Element of OAS st not LIN p,a,b &amp; p,a '||' b,c &amp; p,b '||' a,c holds
( p,a // b,c &amp; p,b // a,c )
proofend;

theorem Th15: :: PASCH:15
for OAS being OAffinSpace
for p, c, b, d, a being Element of OAS st Mid p,c,b &amp; c,d // b,a &amp; p,d // p,a &amp; not LIN p,a,b &amp; p <> c holds
Mid p,d,a
proofend;

theorem Th16: :: PASCH:16
for OAS being OAffinSpace
for p, d, a, c, b being Element of OAS st Mid p,d,a &amp; c,d // b,a &amp; p,c // p,b &amp; not LIN p,a,b &amp; p <> c holds
Mid p,c,b
proofend;

theorem Th17: :: PASCH:17
for OAS being OAffinSpace
for p, a, b, c, d being Element of OAS st not LIN p,a,b &amp; p,b // p,c &amp; b,a // c,d &amp; p <> d holds
not Mid a,p,d
proofend;

theorem Th18: :: PASCH:18
for OAS being OAffinSpace
for p, b, c, a being Element of OAS st p,b // p,c &amp; b <> p holds
ex x being Element of OAS st
( p,a // p,x &amp; b,a // c,x )
proofend;

theorem Th19: :: PASCH:19
for OAS being OAffinSpace
for p, c, b, a being Element of OAS st Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a &amp; b,a // c,x )
proofend;

theorem Th20: :: PASCH:20
for OAS being OAffinSpace
for p, b, c, a being Element of OAS st p <> b &amp; Mid p,b,c holds
ex x being Element of OAS st
( Mid p,a,x &amp; b,a // c,x )
proofend;

theorem Th21: :: PASCH:21
for OAS being OAffinSpace
for p, a, b, c being Element of OAS st not LIN p,a,b &amp; Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a &amp; a,b // x,c )
proofend;

theorem :: PASCH:22
for OAS being OAffinSpace
for a, b, c being Element of OAS ex x being Element of OAS st
( a,x // b,c &amp; a,b // x,c )
proofend;

theorem Th23: :: PASCH:23
for OAS being OAffinSpace
for a, b, c, d being Element of OAS st a,b // c,d &amp; not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d &amp; Mid b,x,c )
proofend;

theorem :: PASCH:24
for OAS being OAffinSpace holds OAS is Fanoian
proofend;

theorem :: PASCH:25
for OAS being OAffinSpace
for a, b, c, d being Element of OAS st a,b '||' c,d &amp; a,c '||' b,d &amp; not LIN a,b,c holds
ex x being Element of OAS st
( LIN x,a,d &amp; LIN x,b,c )
proofend;

theorem :: PASCH:26
for OAS being OAffinSpace
for a, b, c, d, p being Element of OAS st a,b '||' c,d &amp; not LIN a,b,c &amp; LIN p,a,d &amp; LIN p,b,c holds
not LIN p,a,b
proofend;

theorem Th27: :: PASCH:27
for OAS being OAffinSpace
for a, b, d, x, c being Element of OAS st Mid a,b,d &amp; Mid b,x,c &amp; not LIN a,b,c holds
ex y being Element of OAS st
( Mid a,y,c &amp; Mid y,x,d )
proofend;

theorem :: PASCH:28
for OAS being OAffinSpace holds OAS is satisfying_Ext_Bet_Pasch
proofend;

theorem Th29: :: PASCH:29
for OAS being OAffinSpace
for a, b, d, x, c being Element of OAS st Mid a,b,d &amp; Mid a,x,c &amp; not LIN a,b,c holds
ex y being Element of OAS st
( Mid b,y,c &amp; Mid x,y,d )
proofend;

theorem :: PASCH:30
for OAS being OAffinSpace holds OAS is satisfying_Int_Bet_Pasch
proofend;

theorem :: PASCH:31
for OAS being OAffinSpace
for p, a, b, p9, a9, b9 being Element of OAS st Mid p,a,b &amp; p,a // p9,a9 &amp; not LIN p,a,p9 &amp; LIN p9,a9,b9 &amp; p,p9 // a,a9 &amp; p,p9 // b,b9 holds
Mid p9,a9,b9
proofend;