:: PASCH semantic presentation

definition

let c₁ be OAffinSpace;
attr a₁ is satisfying_Int_Par_Pasch means :: PASCH:def 1
for b₁, b₂, b₃, b₄, b₅ being Element of a₁ st not LIN b₅,b₂,b₃ & Mid b₂,b₅,b₁ & LIN b₅,b₃,b₄ & b₂,b₃ '||' b₄,b₁ holds
Mid b₃,b₅,b₄;

end;

:: deftheorem Def1 defines satisfying_Int_Par_Pasch PASCH:def 1 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Int_Par_Pasch for satisfying_Int_Par_Pasch c₁c₁ satisfies_Int_Par_Pasch satisfies_Int_Par_Pasch ;

end;

definition

let c₁ be OAffinSpace;
attr a₁ is satisfying_Ext_Par_Pasch means :: PASCH:def 2
for b₁, b₂, b₃, b₄, b₅ being Element of a₁ st Mid b₅,b₂,b₃ & LIN b₅,b₁,b₄ & b₁,b₂ '||' b₃,b₄ & not LIN b₅,b₁,b₂ holds
Mid b₅,b₁,b₄;

end;

:: deftheorem Def2 defines satisfying_Ext_Par_Pasch PASCH:def 2 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Ext_Par_Pasch for satisfying_Ext_Par_Pasch c₁c₁ satisfies_Ext_Par_Pasch satisfies_Ext_Par_Pasch ;

end;

definition

let c₁ be OAffinSpace;
attr a₁ is satisfying_Gen_Par_Pasch means :: PASCH:def 3
for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st not LIN b₁,b₂,b₄ & b₁,b₄ '||' b₂,b₅ & b₁,b₄ '||' b₃,b₆ & Mid b₁,b₂,b₃ & LIN b₄,b₅,b₆ holds
Mid b₄,b₅,b₆;

end;

:: deftheorem Def3 defines satisfying_Gen_Par_Pasch PASCH:def 3 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Gen_Par_Pasch for satisfying_Gen_Par_Pasch c₁c₁ satisfies_Gen_Par_Pasch satisfies_Gen_Par_Pasch ;

end;

definition

let c₁ be OAffinSpace;
attr a₁ is satisfying_Ext_Bet_Pasch means :: PASCH:def 4
for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st Mid b₁,b₂,b₄ & Mid b₂,b₅,b₃ & not LIN b₁,b₂,b₃ holds
ex b₇ being Element of a₁ st
( Mid b₁,b₇,b₃ & Mid b₇,b₅,b₄ );

end;

:: deftheorem Def4 defines satisfying_Ext_Bet_Pasch PASCH:def 4 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Ext_Bet_Pasch for satisfying_Ext_Bet_Pasch c₁c₁ satisfies_Ext_Bet_Pasch satisfies_Ext_Bet_Pasch ;

end;

definition

let c₁ be OAffinSpace;
attr a₁ is satisfying_Int_Bet_Pasch means :: PASCH:def 5
for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st Mid b₁,b₂,b₄ & Mid b₁,b₅,b₃ & not LIN b₁,b₂,b₃ holds
ex b₇ being Element of a₁ st
( Mid b₂,b₇,b₃ & Mid b₅,b₇,b₄ );

end;

:: deftheorem Def5 defines satisfying_Int_Bet_Pasch PASCH:def 5 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Int_Bet_Pasch for satisfying_Int_Bet_Pasch c₁c₁ satisfies_Int_Bet_Pasch satisfies_Int_Bet_Pasch ;

end;

definition

let c₁ be OAffinSpace;
attr a₁ is Fanoian means :: PASCH:def 6
for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ & b₁,b₃ // b₂,b₄ & not LIN b₁,b₂,b₃ holds
ex b₅ being Element of a₁ st
( Mid b₁,b₅,b₄ & Mid b₂,b₅,b₃ );

end;

:: deftheorem Def6 defines Fanoian PASCH:def 6 :

notation

let c₁ be OAffinSpace;
synonym c₁ satisfies_Fano for Fanoian c₁c₁ satisfies_Fano satisfies_Fano ;

end;

theorem Th1: :: PASCH:1

canceled;

theorem Th2: :: PASCH:2

canceled;

theorem Th3: :: PASCH:3

canceled;

theorem Th4: :: PASCH:4

canceled;

theorem Th5: :: PASCH:5

canceled;

theorem Th6: :: PASCH:6

canceled;

theorem Th7: :: PASCH:7

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₃,b₄ & b₃ <> b₄ & b₂ <> b₃ holds
ex b₆ being Element of b₁ st
( b₅,b₃ // b₃,b₆ & b₅,b₂ '||' b₄,b₆ & b₄ <> b₆ & b₃ <> b₆ )

proof end;

theorem Th8: :: PASCH:8

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₂,b₄ & b₂ <> b₄ & b₃ <> b₂ holds
ex b₆ being Element of b₁ st
( b₂,b₅ // b₂,b₆ & b₅,b₃ '||' b₄,b₆ & b₄ <> b₆ )

proof end;

theorem Th9: :: PASCH:9

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ '||' b₂,b₄ & b₂ <> b₃ holds
ex b₆ being Element of b₁ st
( b₂,b₅ '||' b₂,b₆ & b₅,b₃ '||' b₄,b₆ )

proof end;

theorem Th10: :: PASCH:10

canceled;

theorem Th11: :: PASCH:11

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not LIN b₂,b₃,b₄ & LIN b₂,b₄,b₅ & LIN b₂,b₃,b₆ & LIN b₂,b₃,b₇ & b₃,b₄ '||' b₅,b₆ & b₃,b₄ '||' b₅,b₇ holds
b₆ = b₇

proof end;

theorem Th12: :: PASCH:12

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ '||' b₄,b₅ & b₂,b₃ '||' b₄,b₆ & b₂,b₄ '||' b₃,b₅ & b₂,b₄ '||' b₃,b₆ holds
b₅ = b₆

proof end;

theorem Th13: :: PASCH:13

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & Mid b₃,b₂,b₅ & LIN b₂,b₄,b₆ & b₃,b₄ '||' b₆,b₅ holds
Mid b₄,b₂,b₆

proof end;

theorem Th14: :: PASCH:14

for b₁ being OAffinSpace holds b₁ is satisfying_Int_Par_Pasch

proof end;

theorem Th15: :: PASCH:15

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & LIN b₂,b₅,b₆ & b₅,b₃ '||' b₄,b₆ & not LIN b₂,b₅,b₃ holds
Mid b₂,b₅,b₆

proof end;

theorem Th16: :: PASCH:16

for b₁ being OAffinSpace holds b₁ is satisfying_Ext_Par_Pasch

proof end;

theorem Th17: :: PASCH:17

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₄ '||' b₃,b₅ & b₂,b₄ '||' b₆,b₇ & Mid b₂,b₃,b₆ & LIN b₄,b₅,b₇ holds
Mid b₄,b₅,b₇

proof end;

theorem Th18: :: PASCH:18

for b₁ being OAffinSpace holds b₁ is satisfying_Gen_Par_Pasch

proof end;

theorem Th19: :: PASCH:19

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₃,b₂ // b₂,b₅ & b₄,b₂ // b₂,b₆ & b₃,b₄ '||' b₅,b₆ holds
b₃,b₄ // b₆,b₅

proof end;

theorem Th20: :: PASCH:20

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ // b₂,b₅ & b₂,b₄ // b₂,b₆ & b₃,b₄ '||' b₅,b₆ holds
b₃,b₄ // b₅,b₆

proof end;

theorem Th21: :: PASCH:21

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ '||' b₄,b₅ & b₂,b₄ '||' b₃,b₅ holds
( b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ )

proof end;

theorem Th22: :: PASCH:22

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & b₃,b₅ // b₄,b₆ & b₂,b₅ // b₂,b₆ & not LIN b₂,b₆,b₄ & b₂ <> b₃ holds
Mid b₂,b₅,b₆

proof end;

theorem Th23: :: PASCH:23

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & b₅,b₃ // b₆,b₄ & b₂,b₅ // b₂,b₆ & not LIN b₂,b₄,b₆ & b₂ <> b₅ holds
Mid b₂,b₅,b₆

proof end;

theorem Th24: :: PASCH:24

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₄ // b₂,b₅ & b₄,b₃ // b₅,b₆ & LIN b₃,b₂,b₆ & b₂ <> b₆ holds
not Mid b₃,b₂,b₆

proof end;

theorem Th25: :: PASCH:25

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₂,b₄ & b₃ <> b₂ holds
ex b₆ being Element of b₁ st
( b₂,b₅ // b₂,b₆ & b₃,b₅ // b₄,b₆ )

proof end;

theorem Th26: :: PASCH:26

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( Mid b₂,b₆,b₅ & b₄,b₅ // b₃,b₆ )

proof end;

theorem Th27: :: PASCH:27

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & Mid b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( Mid b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ )

proof end;

theorem Th28: :: PASCH:28

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st not LIN b₂,b₃,b₄ & Mid b₂,b₅,b₄ holds
ex b₆ being Element of b₁ st
( Mid b₂,b₆,b₃ & b₃,b₄ // b₆,b₅ )

proof end;

theorem Th29: :: PASCH:29

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂,b₅ // b₃,b₄ & b₂,b₃ // b₅,b₄ )

proof end;

theorem Th30: :: PASCH:30

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ & not LIN b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( Mid b₂,b₆,b₅ & Mid b₃,b₆,b₄ )

proof end;

theorem Th31: :: PASCH:31

canceled;

theorem Th32: :: PASCH:32

for b₁ being OAffinSpace holds b₁ is Fanoian

proof end;

theorem Th33: :: PASCH:33

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ '||' b₄,b₅ & b₂,b₄ '||' b₃,b₅ & not LIN b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( LIN b₆,b₂,b₅ & LIN b₆,b₃,b₄ )

proof end;

theorem Th34: :: PASCH:34

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂,b₃ '||' b₄,b₅ & b₂,b₄ '||' b₃,b₅ & not LIN b₂,b₃,b₄ & LIN b₆,b₂,b₅ & LIN b₆,b₃,b₄ holds
not LIN b₆,b₂,b₃

proof end;

theorem Th35: :: PASCH:35

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₃,b₅,b₆ & not LIN b₂,b₃,b₆ holds
ex b₇ being Element of b₁ st
( Mid b₂,b₇,b₆ & Mid b₇,b₅,b₄ )

proof end;

theorem Th36: :: PASCH:36

for b₁ being OAffinSpace holds b₁ is satisfying_Ext_Bet_Pasch

proof end;

theorem Th37: :: PASCH:37

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₅,b₆ & not LIN b₂,b₃,b₆ holds
ex b₇ being Element of b₁ st
( Mid b₃,b₇,b₆ & Mid b₅,b₇,b₄ )

proof end;

theorem Th38: :: PASCH:38

for b₁ being OAffinSpace holds b₁ is satisfying_Int_Bet_Pasch

proof end;

theorem Th39: :: PASCH:39

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st Mid b₂,b₃,b₄ & b₂,b₃ // b₅,b₆ & not LIN b₂,b₃,b₅ & LIN b₅,b₆,b₇ & b₂,b₅ // b₃,b₆ & b₂,b₅ // b₄,b₇ holds
Mid b₅,b₆,b₇

proof end;