:: PASCH semantic presentation

definition

let OAS be OAffinSpace;
attr OAS 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 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Int_Par_Pasch for satisfying_Int_Par_Pasch OASOAS satisfies_Int_Par_Pasch satisfies_Int_Par_Pasch ;

end;

definition

let OAS be OAffinSpace;
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 & 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 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Ext_Par_Pasch for satisfying_Ext_Par_Pasch OASOAS satisfies_Ext_Par_Pasch satisfies_Ext_Par_Pasch ;

end;

definition

let OAS be OAffinSpace;
attr OAS is satisfying_Gen_Par_Pasch means :: PASCH:def 3
for a, b, c, a', b', c' being Element of OAS 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';

end;

:: deftheorem defines satisfying_Gen_Par_Pasch PASCH:def 3 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Gen_Par_Pasch for satisfying_Gen_Par_Pasch OASOAS satisfies_Gen_Par_Pasch satisfies_Gen_Par_Pasch ;

end;

definition

let OAS be OAffinSpace;
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 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 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Ext_Bet_Pasch for satisfying_Ext_Bet_Pasch OASOAS satisfies_Ext_Bet_Pasch satisfies_Ext_Bet_Pasch ;

end;

definition

let OAS be OAffinSpace;
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 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 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Int_Bet_Pasch for satisfying_Int_Bet_Pasch OASOAS satisfies_Int_Bet_Pasch satisfies_Int_Bet_Pasch ;

end;

definition

let OAS be OAffinSpace;
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 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 :

notation

let OAS be OAffinSpace;
synonym OAS satisfies_Fano for Fanoian OASOAS satisfies_Fano satisfies_Fano ;

end;

theorem :: PASCH:1

canceled;

theorem :: PASCH:2

canceled;

theorem :: PASCH:3

canceled;

theorem :: PASCH:4

canceled;

theorem :: PASCH:5

canceled;

theorem :: PASCH:6

canceled;

theorem Th7: :: PASCH:7

for OAS being OAffinSpace
for b, p, c, a 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 Th8: :: PASCH:8

for OAS being OAffinSpace
for p, b, c, a 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:9

for OAS being OAffinSpace
for p, b, c, a 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 :: PASCH:10

canceled;

theorem Th11: :: PASCH:11

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

proof end;

theorem Th12: :: PASCH:12

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

proof end;

theorem Th13: :: PASCH:13

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

proof end;

theorem :: PASCH:14

for OAS being OAffinSpace holds OAS is satisfying_Int_Par_Pasch

proof end;

theorem Th15: :: PASCH:15

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

proof end;

theorem :: PASCH:16

for OAS being OAffinSpace holds OAS is satisfying_Ext_Par_Pasch

proof end;

theorem Th17: :: PASCH:17

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

proof end;

theorem :: PASCH:18

for OAS being OAffinSpace holds OAS is satisfying_Gen_Par_Pasch

proof end;

theorem :: PASCH:19

for OAS being OAffinSpace
for p, a, b, a', b' being Element of OAS st not LIN p,a,b & a,p // p,a' & b,p // p,b' & a,b '||' a',b' holds
a,b // b',a'

proof end;

theorem :: PASCH:20

for OAS being OAffinSpace
for p, a, a', b, b' being Element of OAS st not LIN p,a,a' & p,a // p,b & p,a' // p,b' & a,a' '||' b,b' holds
a,a' // b,b'

proof end;

theorem Th21: :: PASCH:21

for OAS being OAffinSpace
for p, a, b, c being Element of OAS st not LIN p,a,b & p,a '||' b,c & p,b '||' a,c holds
( p,a // b,c & p,b // a,c )

proof end;

theorem Th22: :: PASCH:22

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

proof end;

theorem Th23: :: PASCH:23

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

proof end;

theorem Th24: :: PASCH:24

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

proof end;

theorem Th25: :: PASCH:25

for OAS being OAffinSpace
for p, b, c, a 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 Th26: :: PASCH:26

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

proof end;

theorem Th27: :: PASCH:27

for OAS being OAffinSpace
for p, b, c, a 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 Th28: :: PASCH:28

for OAS being OAffinSpace
for p, a, b, c being Element of OAS st not LIN p,a,b & Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )

proof end;

theorem :: PASCH:29

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 )

proof end;

theorem Th30: :: PASCH:30

for OAS being OAffinSpace
for a, b, c, d being Element of OAS st a,b // c,d & not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )

proof end;

theorem :: PASCH:31

canceled;

theorem :: PASCH:32

for OAS being OAffinSpace holds OAS is Fanoian

proof end;

theorem :: PASCH:33

for OAS being OAffinSpace
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
( LIN x,a,d & LIN x,b,c )

proof end;

theorem :: PASCH:34

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

proof end;

theorem Th35: :: PASCH:35

for OAS being OAffinSpace
for a, b, d, x, c 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 )

proof end;

theorem :: PASCH:36

for OAS being OAffinSpace holds OAS is satisfying_Ext_Bet_Pasch

proof end;

theorem Th37: :: PASCH:37

for OAS being OAffinSpace
for a, b, d, x, c 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 )

proof end;

theorem :: PASCH:38

for OAS being OAffinSpace holds OAS is satisfying_Int_Bet_Pasch

proof end;

theorem :: PASCH:39

for OAS being OAffinSpace
for p, a, b, p', a', b' being Element of OAS st 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' holds
Mid p',a',b'

proof end;