:: by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and

::

:: Received May 16, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let OAS be OAffinSpace;

end;
attr OAS is satisfying_Int_Par_Pasch means :: PASCH:def 1

for a, b, c, d, p being Element of OAS 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;

for a, b, c, d, p being Element of OAS 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;

:: 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 p,b,c are_collinear & Mid b,p,a & p,c,d are_collinear & b,c '||' d,a holds

Mid c,p,d );

for OAS being OAffinSpace holds

( OAS is satisfying_Int_Par_Pasch iff for a, b, c, d, p being Element of OAS 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 );

definition

let OAS be OAffinSpace;

end;
attr OAS is satisfying_Ext_Par_Pasch means :: PASCH:def 2

for a, b, c, d, p being Element of OAS 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;

for a, b, c, d, p being Element of OAS 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;

:: 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 & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds

Mid p,a,d );

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 & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds

Mid p,a,d );

definition

let OAS be OAffinSpace;

end;
attr OAS is satisfying_Gen_Par_Pasch means :: PASCH:def 3

for a, b, c, a9, b9, c9 being Element of OAS 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;

for a, b, c, a9, b9, c9 being Element of OAS 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;

:: 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 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 );

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 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 );

definition

let OAS be OAffinSpace;

end;
attr OAS 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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d );

for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid b,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d );

:: 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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d ) );

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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d ) );

definition

let OAS be OAffinSpace;

end;
attr OAS 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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d );

for a, b, c, d, x, y being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d );

:: 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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) );

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 a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) );

definition

let OAS be OAffinSpace;

end;
attr OAS 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 a,b,c are_collinear holds

ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c );

for a, b, c, d being Element of OAS st a,b // c,d & a,c // b,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c );

:: 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 a,b,c are_collinear holds

ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c ) );

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 a,b,c are_collinear 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 a, b, c, p being Element of OAS st b,p // p,c & p <> c & b <> p holds

ex d being Element of OAS st

( a,p // p,d & a,b '||' c,d & c <> d & p <> d )

for a, b, c, p being Element of OAS st b,p // p,c & p <> c & b <> p holds

ex d being Element of OAS st

( a,p // p,d & a,b '||' c,d & c <> d & p <> d )

proof end;

theorem Th2: :: PASCH:2

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st p,b // p,c & p <> c & b <> p holds

ex d being Element of OAS st

( p,a // p,d & a,b '||' c,d & c <> d )

for a, b, c, p being Element of OAS st p,b // p,c & p <> c & b <> p holds

ex d being Element of OAS st

( p,a // p,d & a,b '||' c,d & c <> d )

proof end;

theorem :: PASCH:3

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st p,b '||' p,c & p <> b holds

ex d being Element of OAS st

( p,a '||' p,d & a,b '||' c,d )

for a, b, c, p being Element of OAS st p,b '||' p,c & p <> b holds

ex d being Element of OAS st

( p,a '||' p,d & a,b '||' c,d )

proof end;

theorem Th4: :: PASCH:4

for OAS being OAffinSpace

for a, b, c, d1, d2, p being Element of OAS st 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 holds

d1 = d2

for a, b, c, d1, d2, p being Element of OAS st 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 holds

d1 = d2

proof end;

theorem Th5: :: PASCH:5

for OAS being OAffinSpace

for a, b, c, d1, d2 being Element of OAS st not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 holds

d1 = d2

for a, b, c, d1, d2 being Element of OAS st not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 holds

d1 = d2

proof end;

theorem Th6: :: PASCH:6

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS 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

for a, b, c, d, p being Element of OAS 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

proof end;

theorem Th8: :: PASCH:8

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS 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

for a, b, c, d, p being Element of OAS 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

proof end;

theorem Th10: :: PASCH:10

for OAS being OAffinSpace

for a, a9, b, b9, c, c9 being Element of OAS 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

for a, a9, b, b9, c, c9 being Element of OAS 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

proof end;

theorem :: PASCH:12

for OAS being OAffinSpace

for a, a9, b, b9, p being Element of OAS st not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds

a,b // b9,a9

for a, a9, b, b9, p being Element of OAS st not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds

a,b // b9,a9

proof end;

theorem :: PASCH:13

for OAS being OAffinSpace

for a, a9, b, b9, p being Element of OAS st not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds

a,a9 // b,b9

for a, a9, b, b9, p being Element of OAS st not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds

a,a9 // b,b9

proof end;

theorem Th14: :: PASCH:14

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c holds

( p,a // b,c & p,b // a,c )

for a, b, c, p being Element of OAS st not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c holds

( p,a // b,c & p,b // a,c )

proof end;

theorem Th15: :: PASCH:15

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS st Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p <> c holds

Mid p,d,a

for a, b, c, d, p being Element of OAS st Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p <> c holds

Mid p,d,a

proof end;

theorem Th16: :: PASCH:16

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS st Mid p,d,a & c,d // b,a & p,c // p,b & not p,a,b are_collinear & p <> c holds

Mid p,c,b

for a, b, c, d, p being Element of OAS st Mid p,d,a & c,d // b,a & p,c // p,b & not p,a,b are_collinear & p <> c holds

Mid p,c,b

proof end;

theorem Th17: :: PASCH:17

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS st not p,a,b are_collinear & p,b // p,c & b,a // c,d & p <> d holds

not Mid a,p,d

for a, b, c, d, p being Element of OAS st not p,a,b are_collinear & p,b // p,c & b,a // c,d & p <> d holds

not Mid a,p,d

proof end;

theorem Th18: :: PASCH:18

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st p,b // p,c & b <> p holds

ex x being Element of OAS st

( p,a // p,x & b,a // c,x )

for a, b, c, p being Element of OAS st p,b // p,c & b <> p holds

ex x being Element of OAS st

( p,a // p,x & b,a // c,x )

proof end;

theorem Th19: :: PASCH:19

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st Mid p,c,b holds

ex x being Element of OAS st

( Mid p,x,a & b,a // c,x )

for a, b, c, p being Element of OAS st Mid p,c,b holds

ex x being Element of OAS st

( Mid p,x,a & b,a // c,x )

proof end;

theorem Th20: :: PASCH:20

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st p <> b & Mid p,b,c holds

ex x being Element of OAS st

( Mid p,a,x & b,a // c,x )

for a, b, c, p being Element of OAS st p <> b & Mid p,b,c holds

ex x being Element of OAS st

( Mid p,a,x & b,a // c,x )

proof end;

theorem Th21: :: PASCH:21

for OAS being OAffinSpace

for a, b, c, p being Element of OAS st not p,a,b are_collinear & Mid p,c,b holds

ex x being Element of OAS st

( Mid p,x,a & a,b // x,c )

for a, b, c, p being Element of OAS st not p,a,b are_collinear & Mid p,c,b holds

ex x being Element of OAS st

( Mid p,x,a & a,b // x,c )

proof end;

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 & a,b // x,c )

for a, b, c being Element of OAS ex x being Element of OAS st

( a,x // b,c & a,b // x,c )

proof end;

theorem Th23: :: PASCH:23

for OAS being OAffinSpace

for a, b, c, d being Element of OAS st a,b // c,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c )

for a, b, c, d being Element of OAS st a,b // c,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c )

proof end;

theorem :: PASCH:25

for OAS being OAffinSpace

for a, b, c, d being Element of OAS st a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

for a, b, c, d being Element of OAS st a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

proof end;

theorem :: PASCH:26

for OAS being OAffinSpace

for a, b, c, d, p being Element of OAS st a,b '||' c,d & not a,b,c are_collinear & p,a,d are_collinear & p,b,c are_collinear holds

not p,a,b are_collinear

for a, b, c, d, p being Element of OAS st a,b '||' c,d & not a,b,c are_collinear & p,a,d are_collinear & p,b,c are_collinear holds

not p,a,b are_collinear

proof end;

theorem Th27: :: PASCH:27

for OAS being OAffinSpace

for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid b,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d )

for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid b,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid a,y,c & Mid y,x,d )

proof end;

theorem Th29: :: PASCH:29

for OAS being OAffinSpace

for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d )

for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d )

proof end;

theorem :: PASCH:31

for OAS being OAffinSpace

for a, a9, b, b9, p, p9 being Element of OAS st 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 holds

Mid p9,a9,b9

for a, a9, b, b9, p, p9 being Element of OAS st 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 holds

Mid p9,a9,b9

proof end;