:: PASCH semantic presentation 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 & 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 let OAS be OAffinSpace; ::_thesis: 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 ) let b, p, c, a be Element of OAS; ::_thesis: ( b,p // p,c & p <> c & b <> p implies ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) ) assume that A1: b,p // p,c and A2: p <> c and A3: b <> p ; ::_thesis: ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) A4: now__::_thesis:_(_LIN_a,b,p_implies_ex_d_being_Element_of_OAS_st_ (_a,p_//_p,d_&_a,b_'||'_c,d_&_c_<>_d_&_p_<>_d_)_) A5: now__::_thesis:_(_p,a_//_p,b_implies_ex_d_being_Element_of_OAS_st_ (_a,p_//_p,d_&_a,b_'||'_c,d_&_c_<>_d_&_p_<>_d_)_) Mid b,p,c by A1, DIRAF:def_3; then LIN b,p,c by DIRAF:28; then A6: LIN p,c,b by DIRAF:30; assume p,a // p,b ; ::_thesis: ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) then A7: a,p // b,p by DIRAF:2; then a,p // p,c by A1, A3, DIRAF:3; then Mid a,p,c by DIRAF:def_3; then LIN a,p,c by DIRAF:28; then LIN p,c,a by DIRAF:30; then A8: p,c '||' a,b by A6, DIRAF:34; A9: p,c // b,p by A1, DIRAF:2; A10: LIN p,c,c by DIRAF:31; consider d being Element of OAS such that A11: Mid p,c,d and A12: c <> d by DIRAF:13; A13: p <> d by A11, A12, DIRAF:8; p,c // c,d by A11, DIRAF:def_3; then p,c // p,d by ANALOAF:def_5; then A14: b,p // p,d by A2, A9, ANALOAF:def_5; LIN p,c,d by A11, DIRAF:28; then p,c '||' c,d by A10, DIRAF:34; then a,b '||' c,d by A2, A8, DIRAF:23; hence ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A7, A12, A13, A14, DIRAF:3; ::_thesis: verum end; A15: now__::_thesis:_(_p,a_//_b,p_implies_ex_d_being_Element_of_OAS_st_ (_a,p_//_p,d_&_a,b_'||'_c,d_&_c_<>_d_&_p_<>_d_)_) assume p,a // b,p ; ::_thesis: ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) then A16: a,p // p,b by DIRAF:2; then Mid a,p,b by DIRAF:def_3; then LIN a,p,b by DIRAF:28; then A17: LIN p,b,a by DIRAF:30; Mid b,p,c by A1, DIRAF:def_3; then LIN b,p,c by DIRAF:28; then A18: LIN p,b,c by DIRAF:30; A19: LIN a,b,b by DIRAF:31; A20: b <> c by A1, A2, ANALOAF:def_5; LIN p,b,b by DIRAF:31; then LIN a,b,c by A3, A17, A18, DIRAF:32; hence ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A16, A20, A19, DIRAF:34; ::_thesis: verum end; assume LIN a,b,p ; ::_thesis: ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) then LIN p,a,b by DIRAF:30; then p,a '||' p,b by DIRAF:def_5; hence ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A5, A15, DIRAF:def_4; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,p_implies_ex_d_being_Element_of_OAS_st_ (_a,p_//_p,d_&_a,b_'||'_c,d_&_c_<>_d_&_p_<>_d_)_) consider d being Element of OAS such that A21: a,p // p,d and A22: a,b // c,d by A1, A3, ANALOAF:def_5; assume A23: not LIN a,b,p ; ::_thesis: ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) A24: now__::_thesis:_not_d_=_p assume d = p ; ::_thesis: contradiction then p,c // b,a by A22, DIRAF:2; then b,p // b,a by A1, A2, DIRAF:3; then b,p '||' b,a by DIRAF:def_4; then LIN b,p,a by DIRAF:def_5; hence contradiction by A23, DIRAF:30; ::_thesis: verum end; A25: now__::_thesis:_not_d_=_c assume d = c ; ::_thesis: contradiction then p,d // b,p by A1, DIRAF:2; then a,p // b,p by A21, A24, DIRAF:3; then p,a // p,b by DIRAF:2; then p,a '||' p,b by DIRAF:def_4; then LIN p,a,b by DIRAF:def_5; hence contradiction by A23, DIRAF:30; ::_thesis: verum end; a,b '||' c,d by A22, DIRAF:def_4; hence ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A21, A24, A25; ::_thesis: verum end; hence ex d being Element of OAS st ( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A4; ::_thesis: verum end; theorem Th2: :: PASCH:2 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, b, c, a be Element of OAS; ::_thesis: ( p,b // p,c & p <> c & b <> p implies ex d being Element of OAS st ( p,a // p,d & a,b '||' c,d & c <> d ) ) assume that A1: p,b // p,c and A2: p <> c and A3: b <> p ; ::_thesis: ex d being Element of OAS st ( p,a // p,d & a,b '||' c,d & c <> d ) consider q being Element of OAS such that A4: Mid b,p,q and A5: p <> q by DIRAF:13; A6: b,p // p,q by A4, DIRAF:def_3; then consider r being Element of OAS such that A7: a,p // p,r and A8: a,b '||' q,r and A9: q <> r and A10: r <> p by A3, A5, Th1; b,p // c,p by A1, DIRAF:2; then p,q // c,p by A3, A6, ANALOAF:def_5; then q,p // p,c by DIRAF:2; then consider d being Element of OAS such that A11: r,p // p,d and A12: r,q '||' c,d and A13: c <> d and d <> p by A2, A5, Th1; p,r // d,p by A11, DIRAF:2; then a,p // d,p by A7, A10, DIRAF:3; then A14: p,a // p,d by DIRAF:2; q,r '||' c,d by A12, DIRAF:22; then a,b '||' c,d by A8, A9, DIRAF:23; hence ex d being Element of OAS st ( p,a // p,d & a,b '||' c,d & c <> d ) by A13, A14; ::_thesis: verum end; theorem :: PASCH:3 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, b, c, a be Element of OAS; ::_thesis: ( p,b '||' p,c & p <> b implies ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) ) assume that A1: p,b '||' p,c and A2: p <> b ; ::_thesis: ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) A3: now__::_thesis:_(_p_<>_c_implies_ex_d_being_Element_of_OAS_st_ (_p,a_'||'_p,d_&_a,b_'||'_c,d_)_) assume A4: p <> c ; ::_thesis: ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) A5: now__::_thesis:_(_p,b_//_c,p_implies_ex_d_being_Element_of_OAS_st_ (_p,a_'||'_p,d_&_a,b_'||'_c,d_)_) assume p,b // c,p ; ::_thesis: ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) then b,p // p,c by DIRAF:2; then consider d being Element of OAS such that A6: a,p // p,d and A7: a,b '||' c,d and c <> d and d <> p by A2, A4, Th1; p,a // d,p by A6, DIRAF:2; then p,a '||' p,d by DIRAF:def_4; hence ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) by A7; ::_thesis: verum end; now__::_thesis:_(_p,b_//_p,c_implies_ex_d_being_Element_of_OAS_st_ (_p,a_'||'_p,d_&_a,b_'||'_c,d_)_) assume p,b // p,c ; ::_thesis: ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) then consider d being Element of OAS such that A8: p,a // p,d and A9: a,b '||' c,d and c <> d by A2, A4, Th2; p,a '||' p,d by A8, DIRAF:def_4; hence ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) by A9; ::_thesis: verum end; hence ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) by A1, A5, DIRAF:def_4; ::_thesis: verum end; now__::_thesis:_(_p_=_c_implies_ex_d_being_Element_of_OAS_st_ (_p,a_'||'_p,d_&_a,b_'||'_c,d_)_) A10: a,b '||' p,p by DIRAF:20; A11: p,a '||' p,p by DIRAF:20; assume p = c ; ::_thesis: ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) hence ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) by A11, A10; ::_thesis: verum end; hence ex d being Element of OAS st ( p,a '||' p,d & a,b '||' c,d ) by A3; ::_thesis: verum end; 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 & LIN p,b,c & LIN p,a,d1 & LIN p,a,d2 & a,b '||' c,d1 & a,b '||' c,d2 holds d1 = d2 proof let OAS be OAffinSpace; ::_thesis: 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 let p, a, b, c, d1, d2 be Element of OAS; ::_thesis: ( 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 implies d1 = d2 ) assume that A1: not LIN p,a,b and A2: LIN p,b,c and A3: LIN p,a,d1 and A4: LIN p,a,d2 and A5: a,b '||' c,d1 and A6: a,b '||' c,d2 ; ::_thesis: d1 = d2 A7: p <> a by A1, DIRAF:31; A8: a <> b by A1, DIRAF:31; A9: now__::_thesis:_(_p_<>_c_implies_not_d1_<>_d2_) LIN p,a,a by DIRAF:31; then A10: LIN d1,d2,a by A3, A4, A7, DIRAF:32; A11: LIN d1,d2,d1 by DIRAF:31; A12: LIN p,c,b by A2, DIRAF:30; A13: LIN d1,d2,d2 by DIRAF:31; A14: LIN p,a,p by DIRAF:31; then A15: LIN d1,d2,p by A3, A4, A7, DIRAF:32; c,d1 '||' c,d2 by A5, A6, A8, DIRAF:23; then A16: LIN c,d1,d2 by DIRAF:def_5; then A17: LIN d1,d2,c by DIRAF:30; assume A18: p <> c ; ::_thesis: not d1 <> d2 assume A19: d1 <> d2 ; ::_thesis: contradiction LIN d1,d2,p by A3, A4, A7, A14, DIRAF:32; then A20: LIN p,c,d1 by A19, A17, A11, DIRAF:32; LIN d1,d2,c by A16, DIRAF:30; then LIN p,c,d2 by A19, A15, A13, DIRAF:32; then LIN d1,d2,b by A18, A20, A12, DIRAF:32; hence contradiction by A1, A19, A15, A10, DIRAF:32; ::_thesis: verum end; A21: LIN p,d2,a by A4, DIRAF:30; A22: LIN p,d1,a by A3, DIRAF:30; now__::_thesis:_(_c_=_p_implies_d1_=_d2_) A23: LIN p,d2,p by DIRAF:31; assume A24: c = p ; ::_thesis: d1 = d2 then A25: p,d2 '||' a,b by A6, DIRAF:22; A26: now__::_thesis:_not_p_<>_d2 assume A27: p <> d2 ; ::_thesis: contradiction then LIN p,d2,b by A21, A25, DIRAF:33; hence contradiction by A1, A21, A23, A27, DIRAF:32; ::_thesis: verum end; A28: LIN p,d1,p by DIRAF:31; A29: p,d1 '||' a,b by A5, A24, DIRAF:22; now__::_thesis:_not_p_<>_d1 assume A30: p <> d1 ; ::_thesis: contradiction then LIN p,d1,b by A22, A29, DIRAF:33; hence contradiction by A1, A22, A28, A30, DIRAF:32; ::_thesis: verum end; hence d1 = d2 by A26; ::_thesis: verum end; hence d1 = d2 by A9; ::_thesis: verum end; theorem Th5: :: PASCH:5 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 let OAS be OAffinSpace; ::_thesis: 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 let a, b, c, d1, d2 be Element of OAS; ::_thesis: ( not LIN a,b,c & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 implies d1 = d2 ) assume that A1: not LIN a,b,c and A2: a,b '||' c,d1 and A3: a,b '||' c,d2 and A4: a,c '||' b,d1 and A5: a,c '||' b,d2 ; ::_thesis: d1 = d2 assume A6: d1 <> d2 ; ::_thesis: contradiction a <> c by A1, DIRAF:31; then b,d1 '||' b,d2 by A4, A5, DIRAF:23; then LIN b,d1,d2 by DIRAF:def_5; then A7: LIN d1,d2,b by DIRAF:30; A8: now__::_thesis:_not_c_=_d1 assume c = d1 ; ::_thesis: contradiction then c,a '||' c,b by A4, DIRAF:22; then LIN c,a,b by DIRAF:def_5; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; A9: LIN d1,d2,d1 by DIRAF:31; a <> b by A1, DIRAF:31; then c,d1 '||' c,d2 by A2, A3, DIRAF:23; then A10: LIN c,d1,d2 by DIRAF:def_5; then A11: LIN d1,d2,c by DIRAF:30; LIN d1,d2,c by A10, DIRAF:30; then d1,d2 '||' c,d1 by A9, DIRAF:34; then ( d1,d2 '||' a,b or c = d1 ) by A2, DIRAF:23; then d1,d2 '||' b,a by A8, DIRAF:22; then LIN d1,d2,a by A6, A7, DIRAF:33; hence contradiction by A1, A6, A11, A7, DIRAF:32; ::_thesis: verum end; theorem Th6: :: PASCH:6 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 let OAS be OAffinSpace; ::_thesis: 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 let p, b, c, a, d be Element of OAS; ::_thesis: ( not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a implies Mid c,p,d ) assume that A1: not LIN p,b,c and A2: Mid b,p,a and A3: LIN p,c,d and A4: b,c '||' d,a ; ::_thesis: Mid c,p,d A5: LIN p,d,c by A3, DIRAF:30; LIN b,p,a by A2, DIRAF:28; then A6: LIN p,b,a by DIRAF:30; p,c '||' p,d by A3, DIRAF:def_5; then A7: ( p,c // p,d or p,c // d,p ) by DIRAF:def_4; assume A8: not Mid c,p,d ; ::_thesis: contradiction then A9: d <> p by DIRAF:10; A10: now__::_thesis:_not_p,c_//_d,p assume p,c // d,p ; ::_thesis: contradiction then c,p // p,d by DIRAF:2; hence contradiction by A8, DIRAF:def_3; ::_thesis: verum end; p <> c by A8, DIRAF:10; then consider q being Element of OAS such that A11: p,b // p,q and A12: b,c '||' d,q and d <> q by A9, A7, A10, Th2; A13: LIN p,d,p by DIRAF:31; p,b '||' p,q by A11, DIRAF:def_4; then LIN p,b,q by DIRAF:def_5; then a = q by A1, A3, A4, A12, A6, Th4; then b,p // p,q by A2, DIRAF:def_3; then p,q // b,p by DIRAF:2; then ( p,b // b,p or p = q ) by A11, DIRAF:3; then ( p = b or p = q ) by ANALOAF:def_5; then p,d '||' c,b by A1, A12, DIRAF:22, DIRAF:31; then LIN p,d,b by A9, A5, DIRAF:33; hence contradiction by A1, A9, A5, A13, DIRAF:32; ::_thesis: verum end; theorem :: PASCH:7 for OAS being OAffinSpace holds OAS is satisfying_Int_Par_Pasch proof let OAS be OAffinSpace; ::_thesis: OAS is satisfying_Int_Par_Pasch let a be Element of OAS; :: according to PASCH:def_1 ::_thesis: for 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 let b, c, d, p be Element of OAS; ::_thesis: ( not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a implies Mid c,p,d ) assume that A1: not LIN p,b,c and A2: Mid b,p,a and A3: LIN p,c,d and A4: b,c '||' d,a ; ::_thesis: Mid c,p,d thus Mid c,p,d by A1, A2, A3, A4, Th6; ::_thesis: verum end; theorem Th8: :: PASCH:8 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 let OAS be OAffinSpace; ::_thesis: 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 let p, b, c, a, d be Element of OAS; ::_thesis: ( Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b implies Mid p,a,d ) assume that A1: Mid p,b,c and A2: LIN p,a,d and A3: a,b '||' c,d and A4: not LIN p,a,b ; ::_thesis: Mid p,a,d A5: now__::_thesis:_(_b_<>_c_implies_Mid_p,a,d_) LIN d,a,p by A2, DIRAF:30; then d,a '||' d,p by DIRAF:def_5; then A6: a,d '||' d,p by DIRAF:22; assume A7: b <> c ; ::_thesis: Mid p,a,d A8: b <> a by A4, DIRAF:31; A9: not LIN d,b,a proof assume LIN d,b,a ; ::_thesis: contradiction then A10: LIN a,b,d by DIRAF:30; a,b '||' d,c by A3, DIRAF:22; then LIN a,b,c by A8, A10, DIRAF:33; then A11: LIN b,c,a by DIRAF:30; LIN p,b,c by A1, DIRAF:28; then A12: LIN b,c,p by DIRAF:30; LIN b,c,b by DIRAF:31; hence contradiction by A4, A7, A11, A12, DIRAF:32; ::_thesis: verum end; then d <> a by DIRAF:31; then consider q being Element of OAS such that A13: b,d '||' d,q and A14: b,a '||' p,q by A6, DIRAF:27; A15: LIN p,b,c by A1, DIRAF:28; A16: p <> c by A1, A7, DIRAF:8; A17: not LIN b,c,d proof A18: LIN p,c,c by DIRAF:31; LIN p,b,c by A1, DIRAF:28; then A19: LIN p,c,b by DIRAF:30; assume A20: LIN b,c,d ; ::_thesis: contradiction A21: LIN b,c,b by DIRAF:31; A22: now__::_thesis:_not_a,b_'||'_c,b assume a,b '||' c,b ; ::_thesis: contradiction then b,c '||' b,a by DIRAF:22; then LIN b,c,a by DIRAF:def_5; hence contradiction by A7, A9, A20, A21, DIRAF:32; ::_thesis: verum end; LIN c,d,b by A20, DIRAF:30; then c,d '||' c,b by DIRAF:def_5; then LIN p,a,c by A2, A3, A22, DIRAF:23; then LIN p,c,a by DIRAF:30; then LIN b,c,a by A16, A19, A18, DIRAF:32; hence contradiction by A7, A9, A20, A21, DIRAF:32; ::_thesis: verum end; a,b '||' q,p by A14, DIRAF:22; then A23: c,d '||' q,p by A3, A8, DIRAF:23; d,b '||' d,q by A13, DIRAF:22; then LIN d,b,q by DIRAF:def_5; then A24: LIN b,d,q by DIRAF:30; A25: d <> p proof A26: LIN p,c,p by DIRAF:31; LIN p,b,c by A1, DIRAF:28; then A27: LIN p,c,b by DIRAF:30; assume d = p ; ::_thesis: contradiction then p,c '||' b,a by A3, DIRAF:22; then LIN p,c,a by A16, A27, DIRAF:33; hence contradiction by A4, A16, A27, A26, DIRAF:32; ::_thesis: verum end; A28: not LIN d,p,q proof A29: now__::_thesis:_not_p_=_q assume p = q ; ::_thesis: contradiction then d,b '||' d,p by A13, DIRAF:22; then LIN d,b,p by DIRAF:def_5; then A30: LIN d,p,b by DIRAF:30; A31: LIN d,p,d by DIRAF:31; LIN d,p,a by A2, DIRAF:30; hence contradiction by A9, A25, A31, A30, DIRAF:32; ::_thesis: verum end; A32: LIN p,q,p by DIRAF:31; A33: LIN d,p,p by DIRAF:31; assume A34: LIN d,p,q ; ::_thesis: contradiction LIN d,p,a by A2, DIRAF:30; then A35: LIN p,q,a by A25, A34, A33, DIRAF:32; p,q '||' a,b by A14, DIRAF:22; then LIN p,q,b by A35, A29, DIRAF:33; hence contradiction by A4, A35, A29, A32, DIRAF:32; ::_thesis: verum end; Mid c,b,p by A1, DIRAF:9; then A36: Mid d,b,q by A17, A24, A23, Th6; A37: now__::_thesis:_not_Mid_p,d,a d,b '||' d,q by A13, DIRAF:22; then LIN d,b,q by DIRAF:def_5; then A38: LIN d,q,b by DIRAF:30; assume A39: Mid p,d,a ; ::_thesis: contradiction p,q '||' b,a by A14, DIRAF:22; then Mid q,d,b by A28, A39, A38, Th6; then Mid b,d,q by DIRAF:9; then b = d by A36, DIRAF:14; hence contradiction by A9, DIRAF:31; ::_thesis: verum end; assume not Mid p,a,d ; ::_thesis: contradiction then Mid a,p,d by A2, A37, DIRAF:29; then Mid b,p,c by A3, A4, A15, Th6; then p = b by A1, DIRAF:14; hence contradiction by A4, DIRAF:31; ::_thesis: verum end; now__::_thesis:_(_b_=_c_implies_Mid_p,a,d_) A40: a,b '||' b,a by DIRAF:19; A41: LIN p,a,a by DIRAF:31; A42: LIN p,b,b by DIRAF:31; assume b = c ; ::_thesis: Mid p,a,d then a = d by A2, A3, A4, A42, A41, A40, Th4; hence Mid p,a,d by DIRAF:10; ::_thesis: verum end; hence Mid p,a,d by A5; ::_thesis: verum end; theorem :: PASCH:9 for OAS being OAffinSpace holds OAS is satisfying_Ext_Par_Pasch proof let OAS be OAffinSpace; ::_thesis: OAS is satisfying_Ext_Par_Pasch let a be Element of OAS; :: according to PASCH:def_2 ::_thesis: for 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 let b, c, d, p be Element of OAS; ::_thesis: ( Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b implies Mid p,a,d ) assume that A1: Mid p,b,c and A2: LIN p,a,d and A3: a,b '||' c,d and A4: not LIN p,a,b ; ::_thesis: Mid p,a,d thus Mid p,a,d by A1, A2, A3, A4, Th8; ::_thesis: verum end; 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 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds Mid a9,b9,c9 proof let OAS be OAffinSpace; ::_thesis: for a, b, a9, b9, c, 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 let a, b, a9, b9, c, c9 be Element of OAS; ::_thesis: ( not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 implies Mid a9,b9,c9 ) assume that A1: not LIN a,b,a9 and A2: a,a9 '||' b,b9 and A3: a,a9 '||' c,c9 and A4: Mid a,b,c and A5: LIN a9,b9,c9 ; ::_thesis: Mid a9,b9,c9 A6: LIN a,b,c by A4, DIRAF:28; A7: LIN b9,c9,a9 by A5, DIRAF:30; A8: LIN c9,b9,a9 by A5, DIRAF:30; A9: a <> a9 by A1, DIRAF:31; then A10: b,b9 '||' c,c9 by A2, A3, DIRAF:23; A11: a <> b by A1, DIRAF:31; then A12: a <> c by A4, DIRAF:8; A13: now__::_thesis:_(_b9_<>_c9_&_a9_<>_b9_&_b_<>_b9_implies_Mid_a9,b9,c9_) assume that A14: b9 <> c9 and a9 <> b9 and A15: b <> b9 ; ::_thesis: Mid a9,b9,c9 A16: not LIN b,b9,a9 proof A17: LIN b,b9,b by DIRAF:31; assume A18: LIN b,b9,a9 ; ::_thesis: contradiction b,b9 '||' a9,a by A2, DIRAF:22; then LIN b,b9,a by A15, A18, DIRAF:33; hence contradiction by A1, A15, A18, A17, DIRAF:32; ::_thesis: verum end; A19: now__::_thesis:_(_c_<>_c9_implies_Mid_a9,b9,c9_) a,b '||' a,c by A6, DIRAF:def_5; then c,a '||' a,b by DIRAF:22; then consider x being Element of OAS such that A20: c9,a '||' a,x and A21: c9,c '||' b,x by A12, DIRAF:27; a,c9 '||' a,x by A20, DIRAF:22; then A22: LIN a,c9,x by DIRAF:def_5; assume A23: c <> c9 ; ::_thesis: Mid a9,b9,c9 A24: x <> b proof assume x = b ; ::_thesis: contradiction then A25: LIN a,b,c9 by A22, DIRAF:30; LIN a,b,b by DIRAF:31; then A26: LIN c,c9,b by A11, A6, A25, DIRAF:32; LIN a,b,a by DIRAF:31; then LIN c,c9,a by A11, A6, A25, DIRAF:32; then c,c9 '||' a,b by A26, DIRAF:34; then b,b9 '||' a,b by A10, A23, DIRAF:23; then a,a9 '||' a,b by A2, A15, DIRAF:23; then LIN a,a9,b by DIRAF:def_5; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; c,c9 '||' b,x by A21, DIRAF:22; then b,b9 '||' b,x by A10, A23, DIRAF:23; then A27: LIN b,b9,x by DIRAF:def_5; then LIN b,x,b9 by DIRAF:30; then b,x '||' b,b9 by DIRAF:def_5; then b,x '||' c,c9 by A10, A15, DIRAF:23; then A28: x,b '||' c,c9 by DIRAF:22; A29: x <> b9 proof assume x = b9 ; ::_thesis: contradiction then A30: LIN b9,c9,a by A22, DIRAF:30; A31: a,a9 '||' b9,b by A2, DIRAF:22; LIN b9,c9,b9 by DIRAF:31; then LIN a,a9,b9 by A7, A14, A30, DIRAF:32; then LIN a,a9,b by A9, A31, DIRAF:33; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; A32: not LIN c9,b9,x proof assume LIN c9,b9,x ; ::_thesis: contradiction then A33: LIN b9,x,c9 by DIRAF:30; A34: LIN b9,x,b9 by DIRAF:31; A35: LIN c9,b9,b9 by DIRAF:31; LIN b9,x,b by A27, DIRAF:30; then LIN c9,b9,b by A29, A33, A34, DIRAF:32; hence contradiction by A8, A14, A16, A35, DIRAF:32; ::_thesis: verum end; A36: LIN x,b,b9 by A27, DIRAF:30; A37: not LIN a,x,b proof assume LIN a,x,b ; ::_thesis: contradiction then A38: LIN x,b,a by DIRAF:30; A39: b,b9 '||' a,a9 by A2, DIRAF:22; LIN x,b,b by DIRAF:31; then LIN b,b9,a by A36, A24, A38, DIRAF:32; hence contradiction by A15, A16, A39, DIRAF:33; ::_thesis: verum end; LIN b9,b,x by A27, DIRAF:30; then b9,b '||' b9,x by DIRAF:def_5; then b,b9 '||' b9,x by DIRAF:22; then A40: b9,x '||' a,a9 by A2, A15, DIRAF:23; LIN a,x,c9 by A22, DIRAF:30; then Mid a,x,c9 by A4, A28, A37, Th8; then Mid c9,x,a by DIRAF:9; then Mid c9,b9,a9 by A8, A40, A32, Th8; hence Mid a9,b9,c9 by DIRAF:9; ::_thesis: verum end; ( c = c9 implies Mid a9,b9,c9 ) proof A41: not LIN c9,b9,b proof A42: LIN c9,b9,b9 by DIRAF:31; assume LIN c9,b9,b ; ::_thesis: contradiction hence contradiction by A8, A14, A16, A42, DIRAF:32; ::_thesis: verum end; assume c = c9 ; ::_thesis: Mid a9,b9,c9 then A43: Mid c9,b,a by A4, DIRAF:9; b9,b '||' a,a9 by A2, DIRAF:22; then Mid c9,b9,a9 by A8, A43, A41, Th8; hence Mid a9,b9,c9 by DIRAF:9; ::_thesis: verum end; hence Mid a9,b9,c9 by A19; ::_thesis: verum end; ( b = b9 implies Mid a9,b9,c9 ) proof A44: a,a9 '||' c9,c by A3, DIRAF:22; A45: LIN b9,a9,c9 by A5, DIRAF:30; assume A46: b = b9 ; ::_thesis: Mid a9,b9,c9 then not LIN b9,a,a9 by A1, DIRAF:30; hence Mid a9,b9,c9 by A4, A46, A45, A44, Th6; ::_thesis: verum end; hence Mid a9,b9,c9 by A13, DIRAF:10; ::_thesis: verum end; theorem :: PASCH:11 for OAS being OAffinSpace holds OAS is satisfying_Gen_Par_Pasch proof let OAS be OAffinSpace; ::_thesis: OAS is satisfying_Gen_Par_Pasch let a be Element of OAS; :: according to PASCH:def_3 ::_thesis: for 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 let b, c, a9, b9, c9 be Element of OAS; ::_thesis: ( not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 implies Mid a9,b9,c9 ) assume that A1: not LIN a,b,a9 and A2: a,a9 '||' b,b9 and A3: a,a9 '||' c,c9 and A4: Mid a,b,c and A5: LIN a9,b9,c9 ; ::_thesis: Mid a9,b9,c9 thus Mid a9,b9,c9 by A1, A2, A3, A4, A5, Th10; ::_thesis: verum end; theorem :: PASCH:12 for OAS being OAffinSpace for p, a, b, a9, b9 being Element of OAS st not LIN p,a,b & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds a,b // b9,a9 proof let OAS be OAffinSpace; ::_thesis: for p, a, b, a9, b9 being Element of OAS st not LIN p,a,b & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds a,b // b9,a9 let p, a, b, a9, b9 be Element of OAS; ::_thesis: ( not LIN p,a,b & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 implies a,b // b9,a9 ) assume that A1: not LIN p,a,b and A2: a,p // p,a9 and A3: b,p // p,b9 and A4: a,b '||' a9,b9 ; ::_thesis: a,b // b9,a9 A5: not LIN p,b,a by A1, DIRAF:30; Mid b,p,b9 by A3, DIRAF:def_3; then LIN b,p,b9 by DIRAF:28; then A6: LIN p,b,b9 by DIRAF:30; Mid a,p,a9 by A2, DIRAF:def_3; then LIN a,p,a9 by DIRAF:28; then A7: LIN p,a,a9 by DIRAF:30; A8: b,a '||' a9,b9 by A4, DIRAF:22; a <> p by A1, DIRAF:31; then consider q being Element of OAS such that A9: b,p // p,q and A10: b,a // a9,q by A2, ANALOAF:def_5; Mid b,p,q by A9, DIRAF:def_3; then LIN b,p,q by DIRAF:28; then A11: LIN p,b,q by DIRAF:30; b,a '||' a9,q by A10, DIRAF:def_4; then b,a // a9,b9 by A10, A5, A7, A6, A11, A8, Th4; hence a,b // b9,a9 by DIRAF:2; ::_thesis: verum end; theorem :: PASCH:13 for OAS being OAffinSpace for p, a, a9, b, b9 being Element of OAS st not LIN p,a,a9 & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds a,a9 // b,b9 proof let OAS be OAffinSpace; ::_thesis: for p, a, a9, b, b9 being Element of OAS st not LIN p,a,a9 & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds a,a9 // b,b9 let p, a, a9, b, b9 be Element of OAS; ::_thesis: ( not LIN p,a,a9 & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 implies a,a9 // b,b9 ) assume that A1: not LIN p,a,a9 and A2: p,a // p,b and A3: p,a9 // p,b9 and A4: a,a9 '||' b,b9 ; ::_thesis: a,a9 // b,b9 consider c being Element of OAS such that A5: Mid a,p,c and A6: p <> c by DIRAF:13; A7: a,p // p,c by A5, DIRAF:def_3; A8: a <> p by A1, DIRAF:31; then consider c9 being Element of OAS such that A9: a9,p // p,c9 and A10: a9,a // c,c9 by A7, ANALOAF:def_5; A11: a9,a '||' c9,c by A10, DIRAF:def_4; A12: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then Mid a9,p,c by A9, DIRAF:def_3; then LIN a9,p,c by DIRAF:28; then A13: LIN p,c,a9 by DIRAF:30; LIN a,p,c by A5, DIRAF:28; then A14: LIN p,c,a by DIRAF:30; LIN p,c,p by DIRAF:31; hence contradiction by A1, A6, A14, A13, DIRAF:32; ::_thesis: verum end; p,a // c,p by A7, DIRAF:2; then c,p // p,b by A2, A8, ANALOAF:def_5; then consider b99 being Element of OAS such that A15: c9,p // p,b99 and A16: c9,c // b,b99 by A6, ANALOAF:def_5; A17: a9,a '||' b,b9 by A4, DIRAF:22; A18: p <> c9 proof assume p = c9 ; ::_thesis: contradiction then a9,a '||' c,p by A10, DIRAF:def_4; then A19: p,c '||' a,a9 by DIRAF:22; a,p '||' p,c by A7, DIRAF:def_4; then a,p '||' a,a9 by A6, A19, DIRAF:23; then LIN a,p,a9 by DIRAF:def_5; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; p,a '||' p,b by A2, DIRAF:def_4; then A20: LIN p,a,b by DIRAF:def_5; A21: c9,c // a,a9 by A10, DIRAF:2; a9,p '||' p,c9 by A9, DIRAF:def_4; then A22: p,a9 '||' p,c9 by DIRAF:22; p,a9 '||' p,b9 by A3, DIRAF:def_4; then A23: LIN p,a9,b9 by DIRAF:def_5; c9,p '||' p,b99 by A15, DIRAF:def_4; then p,c9 '||' p,b99 by DIRAF:22; then p,a9 '||' p,b99 by A18, A22, DIRAF:23; then A24: LIN p,a9,b99 by DIRAF:def_5; c9,c '||' b,b99 by A16, DIRAF:def_4; then A25: a9,a '||' b,b99 by A12, A11, DIRAF:23; not LIN p,a9,a by A1, DIRAF:30; then c9,c // b,b9 by A20, A23, A17, A16, A24, A25, Th4; hence a,a9 // b,b9 by A12, A21, ANALOAF:def_5; ::_thesis: verum end; theorem Th14: :: PASCH:14 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, a, b, c be Element of OAS; ::_thesis: ( not LIN p,a,b & p,a '||' b,c & p,b '||' a,c implies ( p,a // b,c & p,b // a,c ) ) assume that A1: not LIN p,a,b and A2: p,a '||' b,c and A3: p,b '||' a,c ; ::_thesis: ( p,a // b,c & p,b // a,c ) consider d being Element of OAS such that A4: p,a // b,d and A5: p,b // a,d and a <> d by ANALOAF:def_5; A6: p,b '||' a,d by A5, DIRAF:def_4; p,a '||' b,d by A4, DIRAF:def_4; hence ( p,a // b,c & p,b // a,c ) by A1, A2, A3, A4, A5, A6, Th5; ::_thesis: verum end; theorem Th15: :: PASCH:15 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 let OAS be OAffinSpace; ::_thesis: 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 let p, c, b, d, a be Element of OAS; ::_thesis: ( Mid p,c,b & c,d // b,a & p,d // p,a & not LIN p,a,b & p <> c implies Mid p,d,a ) assume that A1: Mid p,c,b and A2: c,d // b,a and A3: p,d // p,a and A4: not LIN p,a,b and A5: p <> c ; ::_thesis: Mid p,d,a A6: LIN p,c,b by A1, DIRAF:28; now__::_thesis:_(_Mid_p,a,d_implies_Mid_p,d,a_) assume A7: Mid p,a,d ; ::_thesis: Mid p,d,a A8: now__::_thesis:_(_b_<>_c_&_d_<>_a_implies_Mid_p,d,a_) A9: p <> a by A4, DIRAF:31; assume that A10: b <> c and A11: d <> a ; ::_thesis: Mid p,d,a assume not Mid p,d,a ; ::_thesis: contradiction then Mid p,a,d by A3, DIRAF:7; then p,a // a,d by DIRAF:def_3; then consider e1 being Element of OAS such that A12: c,a // a,e1 and A13: c,p // d,e1 by A9, ANALOAF:def_5; A14: d,e1 // c,p by A13, DIRAF:2; A15: c <> e1 proof assume c = e1 ; ::_thesis: contradiction then Mid c,a,c by A12, DIRAF:def_3; hence contradiction by A4, A6, DIRAF:8; ::_thesis: verum end; Mid b,c,p by A1, DIRAF:9; then A16: b,c // c,p by DIRAF:def_3; then A17: c,p // b,c by DIRAF:2; consider e2 being Element of OAS such that A18: b,a // a,e2 and A19: b,c // e1,e2 by A4, A6, A12, ANALOAF:def_5; consider e3 being Element of OAS such that A20: b,c // e2,e3 and A21: b,e2 // c,e3 and c <> e3 by ANALOAF:def_5; A22: a <> b by A4, DIRAF:31; A23: Mid c,a,e1 by A12, DIRAF:def_3; A24: d <> e1 proof ( Mid p,d,a or Mid p,a,d ) by A3, DIRAF:7; then ( LIN p,d,a or LIN p,a,d ) by DIRAF:28; then A25: LIN d,a,p by DIRAF:30; A26: LIN d,a,a by DIRAF:31; assume d = e1 ; ::_thesis: contradiction then LIN c,a,d by A23, DIRAF:28; then LIN d,a,c by DIRAF:30; then LIN d,a,b by A5, A6, A25, DIRAF:35; hence contradiction by A4, A11, A25, A26, DIRAF:32; ::_thesis: verum end; b,a // b,e2 by A18, ANALOAF:def_5; then A27: c,d // b,e2 by A2, A22, DIRAF:3; b <> e2 by A22, A18, ANALOAF:def_5; then c,d // c,e3 by A21, A27, DIRAF:3; then ( Mid c,d,e3 or Mid c,e3,d ) by DIRAF:7; then ( LIN c,d,e3 or LIN c,e3,d ) by DIRAF:28; then A28: LIN d,e3,c by DIRAF:30; e1,e2 // c,p by A10, A19, A16, ANALOAF:def_5; then A29: e1,e2 // d,e1 by A5, A13, DIRAF:3; then d,e1 // e1,e2 by DIRAF:2; then A30: d,e1 // d,e2 by ANALOAF:def_5; then d,e2 // d,e1 by DIRAF:2; then d,e2 // c,p by A24, A14, DIRAF:3; then d,e2 // b,c by A5, A17, DIRAF:3; then A31: d,e2 // e2,e3 by A10, A20, DIRAF:3; then Mid d,e2,e3 by DIRAF:def_3; then LIN d,e2,e3 by DIRAF:28; then A32: LIN d,e3,e2 by DIRAF:30; A33: d <> e2 by A24, A29, ANALOAF:def_5; then A34: d <> e3 by A31, ANALOAF:def_5; d,e2 // d,e3 by A31, ANALOAF:def_5; then d,e1 // d,e3 by A30, A33, DIRAF:3; then ( Mid d,e1,e3 or Mid d,e3,e1 ) by DIRAF:7; then ( LIN d,e1,e3 or LIN d,e3,e1 ) by DIRAF:28; then A35: LIN d,e3,e1 by DIRAF:30; LIN c,a,e1 by A23, DIRAF:28; then LIN c,e1,a by DIRAF:30; then A36: LIN d,e3,a by A15, A28, A35, DIRAF:35; A37: a <> e1 proof p,a // a,d by A7, DIRAF:def_3; then A38: d,a // a,p by DIRAF:2; assume a = e1 ; ::_thesis: contradiction then c,p // a,p by A11, A13, A38, DIRAF:3; then p,c // p,a by DIRAF:2; then ( Mid p,c,a or Mid p,a,c ) by DIRAF:7; then ( LIN p,c,a or LIN p,a,c ) by DIRAF:28; then A39: LIN p,c,a by DIRAF:30; LIN p,c,p by DIRAF:31; hence contradiction by A4, A5, A6, A39, DIRAF:32; ::_thesis: verum end; A40: a <> e2 proof assume A41: a = e2 ; ::_thesis: contradiction e1,a // a,c by A12, DIRAF:2; then b,c // a,c by A19, A37, A41, DIRAF:3; then c,b // c,a by DIRAF:2; then ( Mid c,b,a or Mid c,a,b ) by DIRAF:7; then ( LIN c,b,a or LIN c,a,b ) by DIRAF:28; then A42: LIN c,b,a by DIRAF:30; A43: LIN c,b,b by DIRAF:31; LIN c,b,p by A6, DIRAF:30; hence contradiction by A4, A10, A42, A43, DIRAF:32; ::_thesis: verum end; Mid b,a,e2 by A18, DIRAF:def_3; then LIN b,a,e2 by DIRAF:28; then LIN a,e2,b by DIRAF:30; then A44: LIN d,e3,b by A40, A36, A32, DIRAF:35; LIN c,b,p by A6, DIRAF:30; then LIN d,e3,p by A10, A28, A44, DIRAF:35; hence contradiction by A4, A34, A36, A44, DIRAF:32; ::_thesis: verum end; A45: LIN p,a,d by A7, DIRAF:28; now__::_thesis:_(_b_=_c_implies_a_=_d_) assume b = c ; ::_thesis: a = d then ( Mid b,d,a or Mid b,a,d ) by A2, DIRAF:7; then ( LIN b,d,a or LIN b,a,d ) by DIRAF:28; then A46: LIN d,a,b by DIRAF:30; A47: LIN d,a,a by DIRAF:31; LIN d,a,p by A45, DIRAF:30; hence a = d by A4, A46, A47, DIRAF:32; ::_thesis: verum end; hence Mid p,d,a by A8, DIRAF:10; ::_thesis: verum end; hence Mid p,d,a by A3, DIRAF:7; ::_thesis: verum end; theorem Th16: :: PASCH:16 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 let OAS be OAffinSpace; ::_thesis: 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 let p, d, a, c, b be Element of OAS; ::_thesis: ( Mid p,d,a & c,d // b,a & p,c // p,b & not LIN p,a,b & p <> c implies Mid p,c,b ) assume that A1: Mid p,d,a and A2: c,d // b,a and A3: p,c // p,b and A4: not LIN p,a,b and A5: p <> c ; ::_thesis: Mid p,c,b A6: p <> d proof assume A7: p = d ; ::_thesis: contradiction c,p // b,p by A3, DIRAF:2; then b,p // b,a by A2, A5, A7, ANALOAF:def_5; then ( Mid b,p,a or Mid b,a,p ) by DIRAF:7; then ( LIN b,p,a or LIN b,a,p ) by DIRAF:28; hence contradiction by A4, DIRAF:30; ::_thesis: verum end; ( Mid p,c,b or Mid p,b,c ) by A3, DIRAF:7; then A8: ( LIN p,c,b or LIN p,b,c ) by DIRAF:28; then A9: LIN p,c,b by DIRAF:30; now__::_thesis:_(_Mid_p,b,c_implies_Mid_p,c,b_) A10: not LIN p,d,c proof assume LIN p,d,c ; ::_thesis: contradiction then A11: LIN p,c,d by DIRAF:30; LIN p,c,p by DIRAF:31; then A12: LIN p,d,b by A5, A9, A11, DIRAF:32; A13: LIN p,d,p by DIRAF:31; LIN p,d,a by A1, DIRAF:28; hence contradiction by A4, A6, A12, A13, DIRAF:32; ::_thesis: verum end; assume A14: Mid p,b,c ; ::_thesis: Mid p,c,b p,d // d,a by A1, DIRAF:def_3; then p,d // p,a by ANALOAF:def_5; then A15: p,a // p,d by DIRAF:2; A16: p <> b by A4, DIRAF:31; b,a // c,d by A2, DIRAF:2; then Mid p,a,d by A14, A15, A16, A10, Th15; then A17: Mid d,a,p by DIRAF:9; Mid a,d,p by A1, DIRAF:9; then c,a // b,a by A2, A17, DIRAF:14; then a,c // a,b by DIRAF:2; then ( Mid a,c,b or Mid a,b,c ) by DIRAF:7; then ( LIN a,c,b or LIN a,b,c ) by DIRAF:28; then A18: LIN b,c,a by DIRAF:30; A19: LIN b,c,b by DIRAF:31; LIN b,c,p by A8, DIRAF:30; then b = c by A4, A18, A19, DIRAF:32; hence Mid p,c,b by DIRAF:10; ::_thesis: verum end; hence Mid p,c,b by A3, DIRAF:7; ::_thesis: verum end; theorem Th17: :: PASCH:17 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 & p <> d holds not Mid a,p,d proof let OAS be OAffinSpace; ::_thesis: for p, a, b, c, d being Element of OAS st not LIN p,a,b & p,b // p,c & b,a // c,d & p <> d holds not Mid a,p,d let p, a, b, c, d be Element of OAS; ::_thesis: ( not LIN p,a,b & p,b // p,c & b,a // c,d & p <> d implies not Mid a,p,d ) assume that A1: not LIN p,a,b and A2: p,b // p,c and A3: b,a // c,d and A4: p <> d ; ::_thesis: not Mid a,p,d assume Mid a,p,d ; ::_thesis: contradiction then Mid d,p,a by DIRAF:9; then A5: d,p // p,a by DIRAF:def_3; then A6: p,d // a,p by DIRAF:2; consider b9 being Element of OAS such that A7: c,p // p,b9 and A8: c,d // a,b9 by A4, A5, ANALOAF:def_5; A9: p <> c proof assume p = c ; ::_thesis: contradiction then b,a // a,p by A3, A4, A6, DIRAF:3; then Mid b,a,p by DIRAF:def_3; hence contradiction by A1, DIRAF:9, DIRAF:28; ::_thesis: verum end; A10: a <> b9 proof assume A11: a = b9 ; ::_thesis: contradiction b,p // c,p by A2, DIRAF:2; then b,p // p,a by A9, A7, A11, DIRAF:3; then Mid b,p,a by DIRAF:def_3; then LIN b,p,a by DIRAF:28; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; p,c // b9,p by A7, DIRAF:2; then p,b // b9,p by A2, A9, DIRAF:3; then A12: b9,p // p,b by DIRAF:2; A13: c <> d proof assume c = d ; ::_thesis: contradiction then p,b // a,p by A2, A4, A6, DIRAF:3; then b,p // p,a by DIRAF:2; then Mid b,p,a by DIRAF:def_3; then LIN b,p,a by DIRAF:28; hence contradiction by A1, DIRAF:30; ::_thesis: verum end; p <> b9 proof assume p = b9 ; ::_thesis: contradiction then b,a // a,p by A3, A13, A8, DIRAF:3; then Mid b,a,p by DIRAF:def_3; hence contradiction by A1, DIRAF:9, DIRAF:28; ::_thesis: verum end; then consider b99 being Element of OAS such that A14: a,p // p,b99 and A15: a,b9 // b,b99 by A12, ANALOAF:def_5; a <> p by A1, DIRAF:31; then A16: a <> b99 by A14, ANALOAF:def_5; b,a // a,b9 by A3, A13, A8, DIRAF:3; then b,a // b,b99 by A15, A10, DIRAF:3; then ( Mid b,a,b99 or Mid b,b99,a ) by DIRAF:7; then ( LIN b,a,b99 or LIN b,b99,a ) by DIRAF:28; then A17: LIN a,b99,b by DIRAF:30; Mid a,p,b99 by A14, DIRAF:def_3; then LIN a,p,b99 by DIRAF:28; then A18: LIN a,b99,p by DIRAF:30; LIN a,b99,a by DIRAF:31; hence contradiction by A1, A18, A16, A17, DIRAF:32; ::_thesis: verum end; theorem Th18: :: PASCH:18 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, b, c, a be Element of OAS; ::_thesis: ( p,b // p,c & b <> p implies ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) ) assume that A1: p,b // p,c and A2: b <> p ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) A3: b,p // c,p by A1, DIRAF:2; A4: now__::_thesis:_(_p_<>_c_&_p_<>_a_implies_ex_x_being_Element_of_OAS_st_ (_p,a_//_p,x_&_b,a_//_c,x_)_) assume that p <> c and A5: p <> a ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) consider e1 being Element of OAS such that A6: Mid a,p,e1 and A7: p <> e1 by DIRAF:13; a,p // p,e1 by A6, DIRAF:def_3; then consider e2 being Element of OAS such that A8: b,p // p,e2 and A9: b,a // e1,e2 by A5, ANALOAF:def_5; Mid e1,p,a by A6, DIRAF:9; then A10: e1,p // p,a by DIRAF:def_3; A11: now__::_thesis:_(_p_=_e2_implies_ex_x_being_Element_of_OAS_st_ (_p,a_//_p,x_&_b,a_//_c,x_)_) A12: now__::_thesis:_(_a,b_//_b,p_implies_ex_x_being_Element_of_OAS_st_ (_p,a_//_p,x_&_b,a_//_c,x_)_) A13: now__::_thesis:_(_b,p_//_a,p_implies_(_p,a_//_p,c_&_b,a_//_c,c_)_) assume b,p // a,p ; ::_thesis: ( p,a // p,c & b,a // c,c ) then a,p // c,p by A2, A3, ANALOAF:def_5; hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; ::_thesis: verum end; assume A14: a,b // b,p ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) then a,b // a,p by ANALOAF:def_5; then ( b,p // a,p or a = b ) by A14, ANALOAF:def_5; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A13, DIRAF:1; ::_thesis: verum end; A15: now__::_thesis:_(_a,p_//_p,b_implies_(_p,a_//_p,p_&_b,a_//_c,p_)_) assume A16: a,p // p,b ; ::_thesis: ( p,a // p,p & b,a // c,p ) then a,p // a,b by ANALOAF:def_5; then a,b // p,b by A5, A16, ANALOAF:def_5; then b,a // b,p by DIRAF:2; hence ( p,a // p,p & b,a // c,p ) by A2, A3, DIRAF:3, DIRAF:4; ::_thesis: verum end; assume p = e2 ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) then b,a // p,a by A7, A10, A9, DIRAF:3; then a,b // a,p by DIRAF:2; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A12, A15, DIRAF:6; ::_thesis: verum end; A17: now__::_thesis:_(_e1_=_e2_&_e2_<>_p_implies_ex_x_being_Element_of_OAS_st_ (_p,a_//_p,x_&_b,a_//_c,x_)_) A18: now__::_thesis:_(_p,a_//_a,b_&_p,c_//_c,a_implies_(_p,a_//_p,c_&_b,a_//_c,c_)_) assume that p,a // a,b and A19: p,c // c,a ; ::_thesis: ( p,a // p,c & b,a // c,c ) p,c // p,a by A19, ANALOAF:def_5; hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; ::_thesis: verum end; A20: now__::_thesis:_(_p,b_//_b,a_&_p,c_//_c,a_implies_(_p,a_//_p,c_&_b,a_//_c,c_)_) assume that p,b // b,a and A21: p,c // c,a ; ::_thesis: ( p,a // p,c & b,a // c,c ) p,c // p,a by A21, ANALOAF:def_5; hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; ::_thesis: verum end; A22: now__::_thesis:_(_p,a_//_a,b_&_p,a_//_a,c_implies_(_p,a_//_p,a_&_b,a_//_c,a_)_) assume that A23: p,a // a,b and A24: p,a // a,c ; ::_thesis: ( p,a // p,a & b,a // c,a ) a,b // a,c by A5, A23, A24, ANALOAF:def_5; hence ( p,a // p,a & b,a // c,a ) by DIRAF:1, DIRAF:2; ::_thesis: verum end; A25: ( p,b // b,a & p,a // a,c implies ( p,a // p,c & b,a // c,c ) ) by ANALOAF:def_5; assume that A26: e1 = e2 and A27: e2 <> p ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) p,e2 // a,p by A10, A26, DIRAF:2; then b,p // a,p by A8, A27, DIRAF:3; then A28: p,b // p,a by DIRAF:2; then p,a // p,c by A1, A2, ANALOAF:def_5; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A28, A25, A20, A22, A18, DIRAF:6; ::_thesis: verum end; now__::_thesis:_(_e1_<>_e2_&_e2_<>_p_implies_ex_x_being_Element_of_OAS_st_ (_p,a_//_p,x_&_b,a_//_c,x_)_) assume that A29: e1 <> e2 and A30: e2 <> p ; ::_thesis: ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) p,b // e2,p by A8, DIRAF:2; then e2,p // p,c by A1, A2, ANALOAF:def_5; then consider x being Element of OAS such that A31: e1,p // p,x and A32: e1,e2 // c,x by A30, ANALOAF:def_5; A33: p,a // p,x by A7, A10, A31, ANALOAF:def_5; b,a // c,x by A9, A29, A32, DIRAF:3; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A33; ::_thesis: verum end; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A17, A11; ::_thesis: verum end; A34: ( p = c implies ( p,a // p,c & b,a // c,c ) ) by DIRAF:4; ( p = a implies ( p,a // p,a & b,a // c,a ) ) by A1, DIRAF:1, DIRAF:2; hence ex x being Element of OAS st ( p,a // p,x & b,a // c,x ) by A34, A4; ::_thesis: verum end; 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 & b,a // c,x ) proof let OAS be OAffinSpace; ::_thesis: 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 ) let p, c, b, a be Element of OAS; ::_thesis: ( Mid p,c,b implies ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) ) A1: ( b = c implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:1, DIRAF:10; assume A2: Mid p,c,b ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) A3: now__::_thesis:_(_p_=_b_implies_(_Mid_p,p,a_&_b,a_//_c,p_)_) assume p = b ; ::_thesis: ( Mid p,p,a & b,a // c,p ) then p = c by A2, DIRAF:8; hence ( Mid p,p,a & b,a // c,p ) by DIRAF:4, DIRAF:10; ::_thesis: verum end; A4: p,c // c,b by A2, DIRAF:def_3; A5: now__::_thesis:_(_p_<>_c_&_p_<>_b_&_b_<>_c_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) assume that A6: p <> c and A7: p <> b and A8: b <> c ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) Mid b,c,p by A2, DIRAF:9; then A9: b,c // c,p by DIRAF:def_3; then A10: b,c // b,p by ANALOAF:def_5; then A11: b,p // c,p by A8, A9, ANALOAF:def_5; A12: now__::_thesis:_(_LIN_p,a,b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) A13: now__::_thesis:_(_Mid_p,a,b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) assume A14: Mid p,a,b ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) A15: now__::_thesis:_(_Mid_p,a,c_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) Mid b,a,p by A14, DIRAF:9; then b,a // a,p by DIRAF:def_3; then A16: a,p // b,a by DIRAF:2; assume Mid p,a,c ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) then Mid c,a,p by DIRAF:9; then c,a // a,p by DIRAF:def_3; then A17: a,p // c,a by DIRAF:2; A18: ( b,a // c,a implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:10; ( a = p implies ( Mid p,p,a & b,a // c,p ) ) by A8, A9, A10, ANALOAF:def_5, DIRAF:10; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A17, A16, A18, ANALOAF:def_5; ::_thesis: verum end; ( Mid p,c,a implies ( Mid p,c,a & b,a // c,c ) ) by DIRAF:4; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A2, A14, A15, DIRAF:17; ::_thesis: verum end; A19: now__::_thesis:_(_Mid_a,p,b_implies_(_Mid_p,p,a_&_b,a_//_c,p_)_) assume Mid a,p,b ; ::_thesis: ( Mid p,p,a & b,a // c,p ) then Mid b,p,a by DIRAF:9; then b,p // p,a by DIRAF:def_3; then b,p // b,a by ANALOAF:def_5; hence ( Mid p,p,a & b,a // c,p ) by A7, A11, ANALOAF:def_5, DIRAF:10; ::_thesis: verum end; A20: now__::_thesis:_(_Mid_p,b,a_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) A21: p,c // p,b by A4, ANALOAF:def_5; assume A22: Mid p,b,a ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) then p,b // b,a by DIRAF:def_3; then p,c // b,a by A7, A21, DIRAF:3; then b,a // c,b by A4, A6, ANALOAF:def_5; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A22; ::_thesis: verum end; assume LIN p,a,b ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A13, A19, A20, DIRAF:29; ::_thesis: verum end; now__::_thesis:_(_not_LIN_p,a,b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_b,a_//_c,x_)_) A23: p,b // p,c by A2, DIRAF:7; assume A24: not LIN p,a,b ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) then p <> b by DIRAF:31; then consider x being Element of OAS such that A25: p,a // p,x and A26: b,a // c,x by A23, Th18; A27: p,x // p,a by A25, DIRAF:2; c,x // b,a by A26, DIRAF:2; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A2, A6, A24, A26, A27, Th15; ::_thesis: verum end; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A12; ::_thesis: verum end; ( p = c implies ( Mid p,p,a & b,a // c,p ) ) by DIRAF:4, DIRAF:10; hence ex x being Element of OAS st ( Mid p,x,a & b,a // c,x ) by A3, A1, A5; ::_thesis: verum end; theorem Th20: :: PASCH:20 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, b, c, a be Element of OAS; ::_thesis: ( p <> b & Mid p,b,c implies ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) ) assume that A1: p <> b and A2: Mid p,b,c ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) A3: p,b // b,c by A2, DIRAF:def_3; then A4: p,b // p,c by ANALOAF:def_5; A5: now__::_thesis:_(_not_LIN_p,a,b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) assume A6: not LIN p,a,b ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) consider x being Element of OAS such that A7: p,a // p,x and A8: b,a // c,x by A1, A4, Th18; A9: p <> c by A1, A2, DIRAF:8; A10: p <> x proof p,b // p,c by A2, DIRAF:7; then A11: c,p // b,p by DIRAF:2; assume p = x ; ::_thesis: contradiction then b,a // b,p by A8, A9, A11, DIRAF:3; then ( Mid b,a,p or Mid b,p,a ) by DIRAF:7; then ( LIN b,a,p or LIN b,p,a ) by DIRAF:28; hence contradiction by A6, DIRAF:30; ::_thesis: verum end; not LIN p,x,c proof ( Mid p,a,x or Mid p,x,a ) by A7, DIRAF:7; then ( LIN p,a,x or LIN p,x,a ) by DIRAF:28; then A12: LIN p,x,a by DIRAF:30; A13: LIN p,x,p by DIRAF:31; LIN p,b,c by A2, DIRAF:28; then A14: LIN p,c,b by DIRAF:30; A15: LIN p,c,p by DIRAF:31; assume LIN p,x,c ; ::_thesis: contradiction then LIN p,c,a by A10, A12, A13, DIRAF:32; hence contradiction by A6, A9, A14, A15, DIRAF:32; ::_thesis: verum end; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by A1, A2, A7, A8, Th15; ::_thesis: verum end; A16: now__::_thesis:_(_LIN_p,a,b_&_c_<>_b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) assume that A17: LIN p,a,b and A18: c <> b ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) A19: now__::_thesis:_(_Mid_p,a,b_implies_(_Mid_p,a,a_&_b,a_//_c,a_)_) assume Mid p,a,b ; ::_thesis: ( Mid p,a,a & b,a // c,a ) then Mid a,b,c by A2, DIRAF:11; then Mid c,b,a by DIRAF:9; then A20: c,b // b,a by DIRAF:def_3; then c,b // c,a by ANALOAF:def_5; hence ( Mid p,a,a & b,a // c,a ) by A18, A20, ANALOAF:def_5, DIRAF:10; ::_thesis: verum end; A21: now__::_thesis:_(_Mid_p,b,a_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) assume Mid p,b,a ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) then A22: p,b // b,a by DIRAF:def_3; A23: now__::_thesis:_(_b,a_//_a,c_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) A24: now__::_thesis:_(_p,a_//_a,c_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) assume p,a // a,c ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) then Mid p,a,c by DIRAF:def_3; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by DIRAF:4; ::_thesis: verum end; A25: now__::_thesis:_(_a_=_b_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,a,x_&_b,a_//_c,x_)_) assume a = b ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) then b,a // c,a by DIRAF:4; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by DIRAF:10; ::_thesis: verum end; p,b // p,a by A22, ANALOAF:def_5; then A26: b,a // p,a by A1, A22, ANALOAF:def_5; assume b,a // a,c ; ::_thesis: ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by A26, A25, A24, ANALOAF:def_5; ::_thesis: verum end; A27: now__::_thesis:_(_b,c_//_c,a_implies_(_Mid_p,a,a_&_b,a_//_c,a_)_) assume A28: b,c // c,a ; ::_thesis: ( Mid p,a,a & b,a // c,a ) then b,c // b,a by ANALOAF:def_5; hence ( Mid p,a,a & b,a // c,a ) by A18, A28, ANALOAF:def_5, DIRAF:10; ::_thesis: verum end; b,a // b,c by A1, A3, A22, ANALOAF:def_5; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by A23, A27, ANALOAF:def_5; ::_thesis: verum end; now__::_thesis:_(_Mid_a,p,b_implies_(_Mid_p,a,a_&_b,a_//_c,a_)_) assume Mid a,p,b ; ::_thesis: ( Mid p,a,a & b,a // c,a ) then Mid a,b,c by A1, A2, DIRAF:12; then Mid c,b,a by DIRAF:9; then A29: c,b // b,a by DIRAF:def_3; then c,b // c,a by ANALOAF:def_5; hence ( Mid p,a,a & b,a // c,a ) by A18, A29, ANALOAF:def_5, DIRAF:10; ::_thesis: verum end; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by A17, A19, A21, DIRAF:29; ::_thesis: verum end; ( c = b implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:1, DIRAF:10; hence ex x being Element of OAS st ( Mid p,a,x & b,a // c,x ) by A5, A16; ::_thesis: verum end; theorem Th21: :: PASCH:21 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 let OAS be OAffinSpace; ::_thesis: 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 ) let p, a, b, c be Element of OAS; ::_thesis: ( not LIN p,a,b & Mid p,c,b implies ex x being Element of OAS st ( Mid p,x,a & a,b // x,c ) ) assume that A1: not LIN p,a,b and A2: Mid p,c,b ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & a,b // x,c ) A3: p <> a by A1, DIRAF:31; A4: LIN p,c,b by A2, DIRAF:28; A5: Mid b,c,p by A2, DIRAF:9; then A6: b,c // c,p by DIRAF:def_3; A7: a <> b by A1, DIRAF:31; A8: now__::_thesis:_(_b_<>_c_&_a_<>_c_&_p_<>_c_implies_ex_x_being_Element_of_OAS_st_ (_Mid_p,x,a_&_a,b_//_x,c_)_) assume that A9: b <> c and A10: a <> c and A11: p <> c ; ::_thesis: ex x being Element of OAS st ( Mid p,x,a & a,b // x,c ) consider e1 being Element of OAS such that A12: Mid b,e1,a and A13: p,a // c,e1 by A5, Th19; A14: not LIN p,c,a proof A15: LIN p,c,p by DIRAF:31; assume LIN p,c,a ; ::_thesis: contradiction hence contradiction by A1, A4, A11, A15, DIRAF:32; ::_thesis: verum end; A16: a <> e1 proof assume a = e1 ; ::_thesis: contradiction then a,p // a,c by A13, DIRAF:2; then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7; then ( LIN a,p,c or LIN a,c,p ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; consider e4 being Element of OAS such that A17: e1,c // c,e4 and A18: e1,b // p,e4 by A6, A9, ANALOAF:def_5; consider e2 being Element of OAS such that A19: a,c // c,e2 and A20: a,b // p,e2 by A6, A9, ANALOAF:def_5; consider e3 being Element of OAS such that A21: p,c // c,e3 and A22: p,a // e2,e3 by A10, A19, ANALOAF:def_5; A23: not LIN a,b,c proof assume LIN a,b,c ; ::_thesis: contradiction then A24: LIN b,c,a by DIRAF:30; A25: LIN b,c,b by DIRAF:31; LIN b,c,p by A4, DIRAF:30; hence contradiction by A1, A9, A24, A25, DIRAF:32; ::_thesis: verum end; A26: c <> e2 proof assume A27: c = e2 ; ::_thesis: contradiction p,c // c,b by A6, DIRAF:2; then a,b // c,b by A11, A20, A27, DIRAF:3; then b,a // b,c by DIRAF:2; then ( Mid b,a,c or Mid b,c,a ) by DIRAF:7; then ( LIN b,a,c or LIN b,c,a ) by DIRAF:28; hence contradiction by A23, DIRAF:30; ::_thesis: verum end; A28: e2 <> e3 proof assume e2 = e3 ; ::_thesis: contradiction then c,e2 // p,c by A21, DIRAF:2; then a,c // p,c by A19, A26, DIRAF:3; then c,a // c,p by DIRAF:2; then ( Mid c,a,p or Mid c,p,a ) by DIRAF:7; then ( LIN c,a,p or LIN c,p,a ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; A29: c <> e1 proof assume c = e1 ; ::_thesis: contradiction then LIN b,c,a by A12, DIRAF:28; hence contradiction by A23, DIRAF:30; ::_thesis: verum end; A30: p <> e4 proof assume p = e4 ; ::_thesis: contradiction then c,e1 // p,c by A17, DIRAF:2; then p,a // p,c by A13, A29, DIRAF:3; then ( Mid p,a,c or Mid p,c,a ) by DIRAF:7; then ( LIN p,a,c or LIN p,c,a ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; Mid e1,c,e4 by A17, DIRAF:def_3; then Mid e4,c,e1 by DIRAF:9; then A31: e4,c // c,e1 by DIRAF:def_3; c,e1 // e2,e3 by A3, A13, A22, ANALOAF:def_5; then A32: e4,c // e2,e3 by A29, A31, DIRAF:3; A33: e2 <> e4 proof assume e2 = e4 ; ::_thesis: contradiction then c,e2 // e1,c by A17, DIRAF:2; then a,c // e1,c by A19, A26, DIRAF:3; then c,e1 // c,a by DIRAF:2; then p,a // c,a by A13, A29, DIRAF:3; then a,p // a,c by DIRAF:2; then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7; then ( LIN a,p,c or LIN a,c,p ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; A34: c <> e3 proof assume c = e3 ; ::_thesis: contradiction then c,e2 // a,p by A22, DIRAF:2; then a,c // a,p by A19, A26, DIRAF:3; then ( Mid a,c,p or Mid a,p,c ) by DIRAF:7; then ( LIN a,c,p or LIN a,p,c ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; A35: p <> e3 by A11, A21, ANALOAF:def_5; A36: not LIN p,e3,e2 proof p,c // c,b by A2, DIRAF:def_3; then A37: p,c // p,b by ANALOAF:def_5; p,c // p,e3 by A21, ANALOAF:def_5; then p,b // p,e3 by A11, A37, ANALOAF:def_5; then ( Mid p,b,e3 or Mid p,e3,b ) by DIRAF:7; then ( LIN p,b,e3 or LIN p,e3,b ) by DIRAF:28; then A38: LIN p,e3,b by DIRAF:30; A39: LIN p,e3,p by DIRAF:31; a,c // a,e2 by A19, ANALOAF:def_5; then ( Mid a,c,e2 or Mid a,e2,c ) by DIRAF:7; then ( LIN a,c,e2 or LIN a,e2,c ) by DIRAF:28; then A40: LIN c,e2,a by DIRAF:30; p,c // p,e3 by A21, ANALOAF:def_5; then ( Mid p,c,e3 or Mid p,e3,c ) by DIRAF:7; then ( LIN p,c,e3 or LIN p,e3,c ) by DIRAF:28; then A41: LIN p,e3,c by DIRAF:30; assume LIN p,e3,e2 ; ::_thesis: contradiction then LIN p,e3,a by A26, A41, A40, DIRAF:35; hence contradiction by A1, A35, A38, A39, DIRAF:32; ::_thesis: verum end; then A42: not LIN e3,e2,p by DIRAF:30; consider e5 being Element of OAS such that A43: e4,e2 // c,e5 and A44: e4,c // e2,e5 and A45: e2 <> e5 by ANALOAF:def_5; A46: b <> e1 proof p,c // c,b by A2, DIRAF:def_3; then A47: c,b // p,c by DIRAF:2; assume b = e1 ; ::_thesis: contradiction then p,a // p,c by A9, A13, A47, DIRAF:3; then ( Mid p,a,c or Mid p,c,a ) by DIRAF:7; then ( LIN p,a,c or LIN p,c,a ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; A48: c <> e4 proof assume A49: c = e4 ; ::_thesis: contradiction p,c // c,b by A2, DIRAF:def_3; then e1,b // c,b by A11, A18, A49, DIRAF:3; then b,e1 // b,c by DIRAF:2; then ( Mid b,e1,c or Mid b,c,e1 ) by DIRAF:7; then ( LIN b,e1,c or LIN b,c,e1 ) by DIRAF:28; then A50: LIN b,e1,c by DIRAF:30; A51: LIN b,e1,b by DIRAF:31; LIN b,e1,a by A12, DIRAF:28; hence contradiction by A23, A46, A50, A51, DIRAF:32; ::_thesis: verum end; A52: c <> e5 proof assume c = e5 ; ::_thesis: contradiction then c,e4 // c,e2 by A44, DIRAF:2; then e1,c // c,e2 by A17, A48, DIRAF:3; then c,e2 // e1,c by DIRAF:2; then a,c // e1,c by A19, A26, DIRAF:3; then c,e1 // c,a by DIRAF:2; then p,a // c,a by A13, A29, DIRAF:3; then a,p // a,c by DIRAF:2; then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7; then ( LIN a,p,c or LIN a,c,p ) by DIRAF:28; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; Mid a,e1,b by A12, DIRAF:9; then A53: a,e1 // e1,b by DIRAF:def_3; then a,e1 // a,b by ANALOAF:def_5; then a,b // e1,b by A16, A53, ANALOAF:def_5; then e1,b // p,e2 by A7, A20, ANALOAF:def_5; then A54: p,e4 // p,e2 by A18, A46, ANALOAF:def_5; Mid p,c,e3 by A21, DIRAF:def_3; then Mid p,e4,e2 by A36, A32, A30, A54, Th16; then A55: p,e4 // e4,e2 by DIRAF:def_3; then p,e4 // p,e2 by ANALOAF:def_5; then A56: p,e2 // e4,e2 by A30, A55, ANALOAF:def_5; then A57: p,e2 // c,e5 by A43, A33, DIRAF:3; p <> e2 proof assume p = e2 ; ::_thesis: contradiction then Mid a,c,p by A19, DIRAF:def_3; hence contradiction by A14, DIRAF:9, DIRAF:28; ::_thesis: verum end; then A58: a,b // e4,e2 by A20, A56, DIRAF:3; then A59: a,b // c,e5 by A43, A33, DIRAF:3; A60: e5 <> e3 proof assume e5 = e3 ; ::_thesis: contradiction then c,e3 // a,b by A59, DIRAF:2; then p,c // a,b by A21, A34, DIRAF:3; then c,p // b,a by DIRAF:2; then b,c // b,a by A6, A11, DIRAF:3; then ( Mid b,c,a or Mid b,a,c ) by DIRAF:7; then ( LIN b,c,a or LIN b,a,c ) by DIRAF:28; hence contradiction by A23, DIRAF:30; ::_thesis: verum end; c,e1 // e4,c by A17, DIRAF:2; then c,e1 // e2,e5 by A44, A48, DIRAF:3; then p,a // e2,e5 by A13, A29, DIRAF:3; then e2,e3 // e2,e5 by A3, A22, ANALOAF:def_5; then ( Mid e2,e3,e5 or Mid e2,e5,e3 ) by DIRAF:7; then ( LIN e2,e3,e5 or LIN e2,e5,e3 ) by DIRAF:28; then A61: LIN e2,e3,e5 by DIRAF:30; Mid p,c,e3 by A21, DIRAF:def_3; then A62: Mid e3,c,p by DIRAF:9; e3,c // c,p by A21, DIRAF:2; then consider x being Element of OAS such that A63: e5,c // c,x and A64: e5,e3 // p,x by A34, ANALOAF:def_5; A65: c,e5 // x,c by A63, DIRAF:2; Mid p,c,e3 by A21, DIRAF:def_3; then Mid e3,c,p by DIRAF:9; then e3,c // c,p by DIRAF:def_3; then e3,c // e3,p by ANALOAF:def_5; then e3,p // e3,c by DIRAF:2; then not Mid e2,e3,e5 by A60, A57, A42, Th17; then ( Mid e3,e2,e5 or Mid e2,e5,e3 ) by A61, DIRAF:29; then ( e3,e2 // e2,e5 or Mid e3,e5,e2 ) by DIRAF:9, DIRAF:def_3; then ( e3,e2 // e3,e5 or e3,e5 // e5,e2 ) by ANALOAF:def_5, DIRAF:def_3; then A66: e3,e5 // e3,e2 by ANALOAF:def_5, DIRAF:2; c,e5 // p,e2 by A57, DIRAF:2; then Mid e3,e5,e2 by A34, A42, A66, A62, Th15; then Mid e2,e5,e3 by DIRAF:9; then A67: e2,e5 // e5,e3 by DIRAF:def_3; then e2,e5 // e2,e3 by ANALOAF:def_5; then e2,e3 // e5,e3 by A45, A67, ANALOAF:def_5; then p,a // e5,e3 by A22, A28, DIRAF:3; then p,a // p,x by A64, A60, DIRAF:3; then A68: p,x // p,a by DIRAF:2; a,b // c,e5 by A43, A33, A58, DIRAF:3; then A69: a,b // x,c by A52, A65, DIRAF:3; then c,x // b,a by DIRAF:2; hence ex x being Element of OAS st ( Mid p,x,a & a,b // x,c ) by A1, A2, A11, A69, A68, Th15; ::_thesis: verum end; A70: ( a = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:4, DIRAF:10; A71: ( p = c implies ( a,b // c,c & Mid p,c,a ) ) by DIRAF:4, DIRAF:10; ( b = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:1, DIRAF:10; hence ex x being Element of OAS st ( Mid p,x,a & a,b // x,c ) by A8, A70, A71; ::_thesis: verum 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 ) proof let OAS be OAffinSpace; ::_thesis: for a, b, c being Element of OAS ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) let a, b, c be Element of OAS; ::_thesis: ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) A1: now__::_thesis:_(_not_LIN_a,b,c_implies_ex_x_being_Element_of_OAS_st_ (_a,x_//_b,c_&_a,b_//_x,c_)_) consider e3 being Element of OAS such that A2: Mid b,c,e3 and A3: c <> e3 by DIRAF:13; A4: b,c // c,e3 by A2, DIRAF:def_3; assume A5: not LIN a,b,c ; ::_thesis: ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) then A6: b <> c by DIRAF:31; then consider e4 being Element of OAS such that A7: a,c // c,e4 and A8: a,b // e3,e4 by A4, ANALOAF:def_5; A9: Mid a,c,e4 by A7, DIRAF:def_3; then Mid e4,c,a by DIRAF:9; then A10: e4,c // c,a by DIRAF:def_3; A11: e4 <> c proof assume A12: e4 = c ; ::_thesis: contradiction e3,c // c,b by A4, DIRAF:2; then a,b // c,b by A3, A8, A12, DIRAF:3; then b,a // b,c by DIRAF:2; then ( Mid b,a,c or Mid b,c,a ) by DIRAF:7; then ( LIN b,a,c or LIN b,c,a ) by DIRAF:28; hence contradiction by A5, DIRAF:30; ::_thesis: verum end; A13: not LIN e4,c,e3 proof LIN b,c,e3 by A2, DIRAF:28; then A14: LIN c,e3,b by DIRAF:30; assume A15: LIN e4,c,e3 ; ::_thesis: contradiction A16: LIN c,e3,c by DIRAF:31; A17: LIN e4,c,c by DIRAF:31; LIN e4,c,a by A9, DIRAF:9, DIRAF:28; then LIN c,e3,a by A11, A15, A17, DIRAF:32; hence contradiction by A5, A3, A14, A16, DIRAF:32; ::_thesis: verum end; b,c // c,e3 by A2, DIRAF:def_3; then A18: c,e3 // b,c by DIRAF:2; consider e1 being Element of OAS such that A19: Mid c,a,e1 and A20: a <> e1 by DIRAF:13; A21: c,a // a,e1 by A19, DIRAF:def_3; A22: a <> c by A5, DIRAF:31; then consider e2 being Element of OAS such that A23: b,a // a,e2 and A24: b,c // e1,e2 by A21, ANALOAF:def_5; c,a // c,e1 by A21, ANALOAF:def_5; then e4,c // c,e1 by A22, A10, DIRAF:3; then A25: Mid e4,c,e1 by DIRAF:def_3; then consider e5 being Element of OAS such that A26: Mid e4,e3,e5 and A27: c,e3 // e1,e5 by A11, Th20; A28: e4 <> e3 proof assume e4 = e3 ; ::_thesis: contradiction then Mid a,c,e3 by A7, DIRAF:def_3; then A29: LIN e3,c,a by DIRAF:9, DIRAF:28; A30: LIN e3,c,c by DIRAF:31; LIN e3,c,b by A2, DIRAF:9, DIRAF:28; hence contradiction by A5, A3, A29, A30, DIRAF:32; ::_thesis: verum end; then A31: e4 <> e5 by A26, DIRAF:8; A32: e1 <> e4 by A25, A11, DIRAF:8; A33: not LIN e1,e4,e3 proof LIN e4,c,e1 by A25, DIRAF:28; then A34: LIN e4,e1,c by DIRAF:30; assume LIN e1,e4,e3 ; ::_thesis: contradiction then A35: LIN e4,e1,e3 by DIRAF:30; LIN e4,e1,e4 by DIRAF:31; hence contradiction by A32, A13, A35, A34, DIRAF:32; ::_thesis: verum end; A36: not LIN e1,e5,e4 proof LIN e4,e3,e5 by A26, DIRAF:28; then A37: LIN e5,e4,e3 by DIRAF:30; assume LIN e1,e5,e4 ; ::_thesis: contradiction then A38: LIN e5,e4,e1 by DIRAF:30; LIN e5,e4,e4 by DIRAF:31; hence contradiction by A31, A33, A38, A37, DIRAF:32; ::_thesis: verum end; then A39: e1 <> e5 by DIRAF:31; Mid e1,c,e4 by A25, DIRAF:9; then consider e6 being Element of OAS such that A40: Mid e1,e6,e5 and A41: e5,e4 // e6,c by A36, Th21; A42: c <> e1 by A19, A20, DIRAF:8; A43: not LIN c,e1,b proof LIN c,a,e1 by A19, DIRAF:28; then A44: LIN c,e1,a by DIRAF:30; A45: LIN c,e1,c by DIRAF:31; assume LIN c,e1,b ; ::_thesis: contradiction hence contradiction by A5, A42, A44, A45, DIRAF:32; ::_thesis: verum end; A46: e5 <> e3 proof assume e5 = e3 ; ::_thesis: contradiction then e3,c // e3,e1 by A27, DIRAF:2; then ( Mid e3,c,e1 or Mid e3,e1,c ) by DIRAF:7; then ( LIN e3,c,e1 or LIN e3,e1,c ) by DIRAF:28; then A47: LIN e3,c,e1 by DIRAF:30; A48: LIN e3,c,c by DIRAF:31; LIN e3,c,b by A2, DIRAF:9, DIRAF:28; hence contradiction by A3, A43, A47, A48, DIRAF:32; ::_thesis: verum end; A49: e1 <> e6 proof Mid e5,e3,e4 by A26, DIRAF:9; then A50: e5,e3 // e3,e4 by DIRAF:def_3; then e5,e3 // e5,e4 by ANALOAF:def_5; then A51: e5,e4 // e3,e4 by A46, A50, ANALOAF:def_5; assume e1 = e6 ; ::_thesis: contradiction then e3,e4 // e1,c by A31, A41, A51, ANALOAF:def_5; then A52: a,b // e1,c by A8, A28, DIRAF:3; Mid e1,a,c by A19, DIRAF:9; then A53: e1,a // a,c by DIRAF:def_3; then e1,a // e1,c by ANALOAF:def_5; then e1,c // a,c by A20, A53, ANALOAF:def_5; then a,b // a,c by A42, A52, DIRAF:3; then ( a,b // b,c or a,c // c,b ) by DIRAF:6; then ( Mid a,b,c or Mid a,c,b ) by DIRAF:def_3; then ( LIN a,b,c or LIN a,c,b ) by DIRAF:28; hence contradiction by A5, DIRAF:30; ::_thesis: verum end; consider x being Element of OAS such that A54: Mid c,x,e6 and A55: e1,e6 // a,x by A19, Th19; e1,e6 // e6,e5 by A40, DIRAF:def_3; then e1,e6 // e1,e5 by ANALOAF:def_5; then e1,e5 // a,x by A55, A49, ANALOAF:def_5; then c,e3 // a,x by A27, A39, DIRAF:3; then A56: a,x // b,c by A3, A18, ANALOAF:def_5; A57: e6 <> c proof assume e6 = c ; ::_thesis: contradiction then x = c by A54, DIRAF:8; then c,a // c,b by A56, DIRAF:2; then ( Mid c,a,b or Mid c,b,a ) by DIRAF:7; then ( LIN c,a,b or LIN c,b,a ) by DIRAF:28; hence contradiction by A5, DIRAF:30; ::_thesis: verum end; A58: a <> e2 proof assume A59: a = e2 ; ::_thesis: contradiction e1,a // a,c by A21, DIRAF:2; then b,c // a,c by A20, A24, A59, DIRAF:3; then c,b // c,a by DIRAF:2; then ( Mid c,b,a or Mid c,a,b ) by DIRAF:7; then ( LIN c,b,a or LIN c,a,b ) by DIRAF:28; hence contradiction by A5, DIRAF:30; ::_thesis: verum end; A60: e6 <> x proof assume e6 = x ; ::_thesis: contradiction then e6,e1 // e6,a by A55, DIRAF:2; then ( Mid e6,e1,a or Mid e6,a,e1 ) by DIRAF:7; then ( LIN e6,e1,a or LIN e6,a,e1 ) by DIRAF:28; then A61: LIN e6,e1,a by DIRAF:30; LIN e1,e6,e5 by A40, DIRAF:28; then A62: LIN e6,e1,e5 by DIRAF:30; b,c // e1,e5 by A3, A4, A27, DIRAF:3; then e1,e2 // e1,e5 by A6, A24, ANALOAF:def_5; then ( Mid e1,e2,e5 or Mid e1,e5,e2 ) by DIRAF:7; then ( LIN e1,e2,e5 or LIN e1,e5,e2 ) by DIRAF:28; then A63: LIN e1,e5,e2 by DIRAF:30; A64: LIN e1,e5,e1 by DIRAF:31; Mid b,a,e2 by A23, DIRAF:def_3; then LIN b,a,e2 by DIRAF:28; then A65: LIN a,e2,b by DIRAF:30; LIN c,a,e1 by A19, DIRAF:28; then A66: LIN a,e1,c by DIRAF:30; LIN e6,e1,e1 by DIRAF:31; then LIN e1,e5,a by A49, A61, A62, DIRAF:32; then A67: LIN a,e1,e2 by A39, A63, A64, DIRAF:32; A68: LIN a,e2,a by DIRAF:31; LIN a,e1,a by DIRAF:31; then LIN a,e2,c by A20, A67, A66, DIRAF:32; hence contradiction by A5, A58, A65, A68, DIRAF:32; ::_thesis: verum end; Mid e6,x,c by A54, DIRAF:9; then A69: e6,x // x,c by DIRAF:def_3; then e6,x // e6,c by ANALOAF:def_5; then A70: e6,c // x,c by A60, A69, ANALOAF:def_5; Mid e5,e3,e4 by A26, DIRAF:9; then A71: e5,e3 // e3,e4 by DIRAF:def_3; then e5,e3 // e5,e4 by ANALOAF:def_5; then e3,e4 // e5,e4 by A46, A71, ANALOAF:def_5; then a,b // e5,e4 by A8, A28, DIRAF:3; then a,b // e6,c by A31, A41, DIRAF:3; then a,b // x,c by A57, A70, DIRAF:3; hence ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) by A56; ::_thesis: verum end; now__::_thesis:_(_LIN_a,b,c_implies_ex_x_being_Element_of_OAS_st_ (_a,x_//_b,c_&_a,b_//_x,c_)_) A72: now__::_thesis:_(_Mid_a,c,b_implies_(_a,a_//_b,c_&_a,b_//_a,c_)_) assume Mid a,c,b ; ::_thesis: ( a,a // b,c & a,b // a,c ) then a,c // c,b by DIRAF:def_3; then a,c // a,b by ANALOAF:def_5; hence ( a,a // b,c & a,b // a,c ) by DIRAF:2, DIRAF:4; ::_thesis: verum end; A73: now__::_thesis:_(_Mid_b,a,c_implies_(_a,c_//_b,c_&_a,b_//_c,c_)_) assume Mid b,a,c ; ::_thesis: ( a,c // b,c & a,b // c,c ) then Mid c,a,b by DIRAF:9; then c,a // a,b by DIRAF:def_3; then c,a // c,b by ANALOAF:def_5; hence ( a,c // b,c & a,b // c,c ) by DIRAF:2, DIRAF:4; ::_thesis: verum end; A74: ( Mid a,b,c implies ( a,b // b,c & a,b // b,c ) ) by DIRAF:def_3; assume LIN a,b,c ; ::_thesis: ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) hence ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) by A74, A73, A72, DIRAF:29; ::_thesis: verum end; hence ex x being Element of OAS st ( a,x // b,c & a,b // x,c ) by A1; ::_thesis: verum end; theorem Th23: :: PASCH:23 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 let OAS be OAffinSpace; ::_thesis: 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 ) let a, b, c, d be Element of OAS; ::_thesis: ( a,b // c,d & not LIN a,b,c implies ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) ) assume that A1: a,b // c,d and A2: not LIN a,b,c ; ::_thesis: ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) A3: now__::_thesis:_(_c_<>_d_implies_ex_x_being_Element_of_OAS_st_ (_Mid_a,x,d_&_Mid_b,x,c_)_) consider e1 being Element of OAS such that A4: a,b // d,e1 and A5: a,d // b,e1 and A6: b <> e1 by ANALOAF:def_5; A7: a <> b by A2, DIRAF:31; then c,d // d,e1 by A1, A4, ANALOAF:def_5; then A8: Mid c,d,e1 by DIRAF:def_3; A9: a <> d proof assume a = d ; ::_thesis: contradiction then b,a // a,c by A1, DIRAF:2; then Mid b,a,c by DIRAF:def_3; then LIN b,a,c by DIRAF:28; hence contradiction by A2, DIRAF:30; ::_thesis: verum end; A10: not LIN a,b,d proof A11: now__::_thesis:_(_a,b_//_a,d_implies_LIN_d,c,a_) assume a,b // a,d ; ::_thesis: LIN d,c,a then c,d // a,d by A1, A7, ANALOAF:def_5; then d,c // d,a by DIRAF:2; then d,c '||' d,a by DIRAF:def_4; hence LIN d,c,a by DIRAF:def_5; ::_thesis: verum end; A12: LIN d,a,a by DIRAF:31; A13: now__::_thesis:_(_a,b_//_d,a_implies_LIN_d,c,a_) assume a,b // d,a ; ::_thesis: LIN d,c,a then c,d // d,a by A1, A7, ANALOAF:def_5; then Mid c,d,a by DIRAF:def_3; then LIN c,d,a by DIRAF:28; hence LIN d,c,a by DIRAF:30; ::_thesis: verum end; assume A14: LIN a,b,d ; ::_thesis: contradiction then A15: LIN d,a,b by DIRAF:30; a,b '||' a,d by A14, DIRAF:def_5; then LIN d,a,c by A11, A13, DIRAF:30, DIRAF:def_4; hence contradiction by A2, A9, A12, A15, DIRAF:32; ::_thesis: verum end; consider e2 being Element of OAS such that A16: c,d // b,e2 and A17: c,b // d,e2 and A18: d <> e2 by ANALOAF:def_5; assume A19: c <> d ; ::_thesis: ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) then a,b // b,e2 by A1, A16, DIRAF:3; then A20: Mid a,b,e2 by DIRAF:def_3; A21: not LIN c,d,b proof A22: now__::_thesis:_not_c,d_//_c,b assume c,d // c,b ; ::_thesis: contradiction then a,b // c,b by A1, A19, DIRAF:3; then b,a // b,c by DIRAF:2; then ( Mid b,a,c or Mid b,c,a ) by DIRAF:7; then ( LIN b,a,c or LIN b,c,a ) by DIRAF:28; hence contradiction by A2, DIRAF:30; ::_thesis: verum end; assume LIN c,d,b ; ::_thesis: contradiction then c,d '||' c,b by DIRAF:def_5; then ( c,d // c,b or c,d // b,c ) by DIRAF:def_4; then a,b // b,c by A1, A19, A22, DIRAF:3; then Mid a,b,c by DIRAF:def_3; hence contradiction by A2, DIRAF:28; ::_thesis: verum end; A23: LIN b,c,c by DIRAF:31; A24: LIN d,a,a by DIRAF:31; A25: c <> e1 proof assume c = e1 ; ::_thesis: contradiction then c,d // d,c by A1, A4, A7, ANALOAF:def_5; hence contradiction by A19, ANALOAF:def_5; ::_thesis: verum end; not LIN c,b,e1 proof LIN c,d,e1 by A8, DIRAF:28; then A26: LIN c,e1,d by DIRAF:30; assume LIN c,b,e1 ; ::_thesis: contradiction then A27: LIN c,e1,b by DIRAF:30; LIN c,e1,c by DIRAF:31; hence contradiction by A25, A21, A27, A26, DIRAF:32; ::_thesis: verum end; then consider x being Element of OAS such that A28: Mid c,x,b and A29: b,e1 // x,d by A8, Th21; A30: Mid b,x,c by A28, DIRAF:9; a,d // x,d by A5, A6, A29, DIRAF:3; then d,a // d,x by DIRAF:2; then ( Mid d,a,x or Mid d,x,a ) by DIRAF:7; then ( LIN d,a,x or LIN d,x,a ) by DIRAF:28; then A31: LIN d,a,x by DIRAF:30; A32: b <> c by A2, DIRAF:31; A33: a <> e2 proof assume a = e2 ; ::_thesis: contradiction then a,b // b,a by A1, A19, A16, DIRAF:3; hence contradiction by A7, ANALOAF:def_5; ::_thesis: verum end; not LIN a,d,e2 proof LIN a,b,e2 by A20, DIRAF:28; then A34: LIN a,e2,b by DIRAF:30; assume LIN a,d,e2 ; ::_thesis: contradiction then A35: LIN a,e2,d by DIRAF:30; LIN a,e2,a by DIRAF:31; hence contradiction by A33, A10, A35, A34, DIRAF:32; ::_thesis: verum end; then consider y being Element of OAS such that A36: Mid a,y,d and A37: d,e2 // y,b by A20, Th21; A38: LIN b,c,b by DIRAF:31; c,b // y,b by A17, A18, A37, DIRAF:3; then b,c // b,y by DIRAF:2; then ( Mid b,c,y or Mid b,y,c ) by DIRAF:7; then ( LIN b,c,y or LIN b,y,c ) by DIRAF:28; then A39: LIN b,c,y by DIRAF:30; A40: LIN c,x,b by A28, DIRAF:28; then LIN b,c,x by DIRAF:30; then A41: LIN x,y,c by A32, A39, A23, DIRAF:32; LIN a,y,d by A36, DIRAF:28; then LIN d,a,y by DIRAF:30; then A42: LIN x,y,a by A9, A31, A24, DIRAF:32; LIN b,c,x by A40, DIRAF:30; then LIN x,y,b by A32, A39, A38, DIRAF:32; then Mid a,x,d by A2, A36, A42, A41, DIRAF:32; hence ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) by A30; ::_thesis: verum end; now__::_thesis:_(_c_=_d_implies_ex_x_being_Element_of_OAS_st_ (_Mid_a,x,d_&_Mid_b,x,c_)_) assume A43: c = d ; ::_thesis: ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) take x = c; ::_thesis: ( Mid a,x,d & Mid b,x,c ) thus ( Mid a,x,d & Mid b,x,c ) by A43, DIRAF:10; ::_thesis: verum end; hence ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) by A3; ::_thesis: verum end; theorem :: PASCH:24 for OAS being OAffinSpace holds OAS is Fanoian proof let OAS be OAffinSpace; ::_thesis: OAS is Fanoian let a be Element of OAS; :: according to PASCH:def_6 ::_thesis: for 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 ) let b, c, d be Element of OAS; ::_thesis: ( a,b // c,d & a,c // b,d & not LIN a,b,c implies ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) ) assume that A1: a,b // c,d and a,c // b,d and A2: not LIN a,b,c ; ::_thesis: ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) thus ex x being Element of OAS st ( Mid a,x,d & Mid b,x,c ) by A1, A2, Th23; ::_thesis: verum 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 LIN a,b,c holds ex x being Element of OAS st ( LIN x,a,d & LIN x,b,c ) proof let OAS be OAffinSpace; ::_thesis: 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 ) let a, b, c, d be Element of OAS; ::_thesis: ( a,b '||' c,d & a,c '||' b,d & not LIN a,b,c implies ex x being Element of OAS st ( LIN x,a,d & LIN x,b,c ) ) assume that A1: a,b '||' c,d and A2: a,c '||' b,d and A3: not LIN a,b,c ; ::_thesis: ex x being Element of OAS st ( LIN x,a,d & LIN x,b,c ) a,b // c,d by A1, A2, A3, Th14; then consider x being Element of OAS such that A4: Mid a,x,d and A5: Mid b,x,c by A3, Th23; LIN b,x,c by A5, DIRAF:28; then A6: LIN x,b,c by DIRAF:30; LIN a,x,d by A4, DIRAF:28; then LIN x,a,d by DIRAF:30; hence ex x being Element of OAS st ( LIN x,a,d & LIN x,b,c ) by A6; ::_thesis: verum end; theorem :: PASCH:26 for OAS being OAffinSpace for a, b, c, d, p being Element of OAS st a,b '||' c,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c holds not LIN p,a,b proof let OAS be OAffinSpace; ::_thesis: for a, b, c, d, p being Element of OAS st a,b '||' c,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c holds not LIN p,a,b let a, b, c, d, p be Element of OAS; ::_thesis: ( a,b '||' c,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c implies not LIN p,a,b ) assume that A1: a,b '||' c,d and A2: not LIN a,b,c and A3: LIN p,a,d and A4: LIN p,b,c ; ::_thesis: not LIN p,a,b A5: LIN p,a,a by DIRAF:31; assume LIN p,a,b ; ::_thesis: contradiction then A6: LIN a,b,d by A2, A3, A4, A5, DIRAF:32; A7: a,b '||' d,c by A1, DIRAF:22; a <> b by A2, DIRAF:31; hence contradiction by A2, A6, A7, DIRAF:33; ::_thesis: verum end; theorem Th27: :: PASCH:27 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 let OAS be OAffinSpace; ::_thesis: 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 ) let a, b, d, x, c be Element of OAS; ::_thesis: ( Mid a,b,d & Mid b,x,c & not LIN a,b,c implies ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) ) assume that A1: Mid a,b,d and A2: Mid b,x,c and A3: not LIN a,b,c ; ::_thesis: ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) A4: now__::_thesis:_(_b_=_d_implies_ex_y_being_Element_of_OAS_st_ (_Mid_a,y,c_&_Mid_d,x,y_&_Mid_a,y,c_&_Mid_y,x,d_)_) assume A5: b = d ; ::_thesis: ex y being Element of OAS st ( Mid a,y,c & Mid d,x,y & Mid a,y,c & Mid y,x,d ) take y = c; ::_thesis: ( Mid a,y,c & Mid d,x,y & Mid a,y,c & Mid y,x,d ) thus ( Mid a,y,c & Mid d,x,y ) by A2, A5, DIRAF:10; ::_thesis: ( Mid a,y,c & Mid y,x,d ) thus ( Mid a,y,c & Mid y,x,d ) by A2, A5, DIRAF:9, DIRAF:10; ::_thesis: verum end; A6: Mid d,b,a by A1, DIRAF:9; A7: now__::_thesis:_(_b_<>_d_&_x_<>_b_implies_ex_y_being_Element_of_OAS_st_ (_Mid_a,y,c_&_Mid_y,x,d_)_) assume that A8: b <> d and A9: x <> b ; ::_thesis: ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) d,b // b,a by A6, DIRAF:def_3; then consider e1 being Element of OAS such that A10: x,b // b,e1 and A11: x,d // a,e1 by A8, ANALOAF:def_5; A12: Mid x,b,e1 by A10, DIRAF:def_3; then A13: Mid e1,b,x by DIRAF:9; then A14: Mid e1,x,c by A2, A9, DIRAF:12; A15: c <> e1 proof assume c = e1 ; ::_thesis: contradiction then Mid x,b,x by A2, A9, A13, DIRAF:8, DIRAF:12; hence contradiction by A9, DIRAF:8; ::_thesis: verum end; A16: x <> e1 by A9, A12, DIRAF:8; A17: not LIN c,a,e1 proof LIN x,b,e1 by A12, DIRAF:28; then A18: LIN x,e1,b by DIRAF:30; assume LIN c,a,e1 ; ::_thesis: contradiction then A19: LIN c,e1,a by DIRAF:30; LIN c,x,e1 by A14, DIRAF:9, DIRAF:28; then A20: LIN c,e1,x by DIRAF:30; A21: LIN c,e1,c by DIRAF:31; LIN c,e1,e1 by DIRAF:31; then LIN c,e1,b by A16, A20, A18, DIRAF:35; hence contradiction by A3, A15, A19, A21, DIRAF:32; ::_thesis: verum end; Mid c,x,e1 by A14, DIRAF:9; then consider y being Element of OAS such that A22: Mid c,y,a and A23: a,e1 // y,x by A17, Th21; a <> e1 by A17, DIRAF:31; then x,d // y,x by A11, A23, DIRAF:3; then d,x // x,y by DIRAF:2; then Mid d,x,y by DIRAF:def_3; then A24: Mid y,x,d by DIRAF:9; Mid a,y,c by A22, DIRAF:9; hence ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) by A24; ::_thesis: verum end; now__::_thesis:_(_b_<>_d_&_x_=_b_implies_ex_y_being_Element_of_OAS_st_ (_Mid_a,y,c_&_Mid_y,x,d_)_) assume that b <> d and A25: x = b ; ::_thesis: ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) take y = a; ::_thesis: ( Mid a,y,c & Mid y,x,d ) thus ( Mid a,y,c & Mid y,x,d ) by A1, A25, DIRAF:10; ::_thesis: verum end; hence ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) by A7, A4; ::_thesis: verum end; theorem :: PASCH:28 for OAS being OAffinSpace holds OAS is satisfying_Ext_Bet_Pasch proof let OAS be OAffinSpace; ::_thesis: OAS is satisfying_Ext_Bet_Pasch let a be Element of OAS; :: according to PASCH:def_4 ::_thesis: for 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 ) let b, c, d, x, y be Element of OAS; ::_thesis: ( Mid a,b,d & Mid b,x,c & not LIN a,b,c implies ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) ) assume that A1: Mid a,b,d and A2: Mid b,x,c and A3: not LIN a,b,c ; ::_thesis: ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) thus ex y being Element of OAS st ( Mid a,y,c & Mid y,x,d ) by A1, A2, A3, Th27; ::_thesis: verum end; theorem Th29: :: PASCH:29 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 let OAS be OAffinSpace; ::_thesis: 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 ) let a, b, d, x, c be Element of OAS; ::_thesis: ( Mid a,b,d & Mid a,x,c & not LIN a,b,c implies ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) ) assume that A1: Mid a,b,d and A2: Mid a,x,c and A3: not LIN a,b,c ; ::_thesis: ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) A4: b <> c by A3, DIRAF:31; A5: a <> b by A3, DIRAF:31; A6: now__::_thesis:_(_b_<>_d_&_x_<>_c_&_a_<>_x_implies_ex_y_being_Element_of_OAS_st_ (_Mid_b,y,c_&_Mid_x,y,d_)_) assume that A7: b <> d and A8: x <> c and A9: a <> x ; ::_thesis: ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) A10: a <> d by A1, A7, DIRAF:8; consider e1 being Element of OAS such that A11: Mid a,d,e1 and A12: x,d // c,e1 by A2, A9, Th20; A13: Mid e1,d,a by A11, DIRAF:9; A14: LIN d,b,a by A1, DIRAF:9, DIRAF:28; A15: not LIN a,x,b proof A16: LIN a,x,a by DIRAF:31; assume A17: LIN a,x,b ; ::_thesis: contradiction LIN a,x,c by A2, DIRAF:28; hence contradiction by A3, A9, A17, A16, DIRAF:32; ::_thesis: verum end; A18: not LIN x,d,a proof assume LIN x,d,a ; ::_thesis: contradiction then A19: LIN d,a,x by DIRAF:30; A20: LIN d,a,a by DIRAF:31; LIN d,a,b by A14, DIRAF:30; hence contradiction by A10, A15, A19, A20, DIRAF:32; ::_thesis: verum end; then A21: x <> d by DIRAF:31; A22: Mid d,b,a by A1, DIRAF:9; Mid b,d,e1 by A1, A11, DIRAF:11; then Mid e1,d,b by DIRAF:9; then Mid e1,b,a by A22, A13, DIRAF:12; then A23: e1,b // b,a by DIRAF:def_3; e1 <> b by A7, A22, A13, DIRAF:14; then consider e2 being Element of OAS such that A24: c,b // b,e2 and A25: c,e1 // a,e2 by A23, ANALOAF:def_5; A26: Mid c,b,e2 by A24, DIRAF:def_3; then A27: LIN c,b,e2 by DIRAF:28; Mid c,x,a by A2, DIRAF:9; then consider y being Element of OAS such that A28: Mid c,y,e2 and A29: a,e2 // x,y by Th19; A30: ( Mid c,b,y or Mid c,y,b ) by A26, A28, DIRAF:17; A31: c <> e2 by A4, A24, ANALOAF:def_5; A32: now__::_thesis:_not_Mid_x,d,y LIN c,b,e2 by A26, DIRAF:28; then A33: LIN c,e2,b by DIRAF:30; LIN c,y,e2 by A28, DIRAF:28; then A34: LIN c,e2,y by DIRAF:30; LIN c,e2,c by DIRAF:31; then A35: LIN b,y,c by A31, A34, A33, DIRAF:32; LIN a,x,c by A2, DIRAF:28; then A36: LIN x,a,c by DIRAF:30; A37: Mid c,x,a by A2, DIRAF:9; assume A38: Mid x,d,y ; ::_thesis: contradiction then consider c9 being Element of OAS such that A39: Mid x,c9,a and A40: Mid c9,b,y by A22, A18, Th27; LIN x,c9,a by A39, DIRAF:28; then A41: LIN x,a,c9 by DIRAF:30; A42: b <> y proof assume b = y ; ::_thesis: contradiction then LIN x,d,b by A38, DIRAF:28; then A43: LIN d,b,x by DIRAF:30; A44: LIN d,b,b by DIRAF:31; LIN a,x,c by A2, DIRAF:28; then LIN d,b,c by A9, A14, A43, DIRAF:35; hence contradiction by A3, A7, A14, A44, DIRAF:32; ::_thesis: verum end; LIN c9,b,y by A40, DIRAF:28; then A45: LIN b,y,c9 by DIRAF:30; then A46: LIN c,c9,c by A42, A35, DIRAF:32; LIN b,y,b by DIRAF:31; then A47: LIN c,c9,b by A42, A35, A45, DIRAF:32; LIN x,a,a by DIRAF:31; then LIN c,c9,a by A9, A36, A41, DIRAF:32; then Mid x,c,a by A3, A39, A47, A46, DIRAF:32; hence contradiction by A8, A37, DIRAF:14; ::_thesis: verum end; A48: a <> e2 proof assume a = e2 ; ::_thesis: contradiction then Mid c,b,a by A24, DIRAF:def_3; hence contradiction by A3, DIRAF:9, DIRAF:28; ::_thesis: verum end; A49: LIN e1,d,a by A11, DIRAF:9, DIRAF:28; A50: c <> e1 proof assume c = e1 ; ::_thesis: contradiction then A51: LIN d,a,c by A49, DIRAF:30; A52: LIN d,a,a by DIRAF:31; LIN d,a,b by A14, DIRAF:30; hence contradiction by A3, A10, A51, A52, DIRAF:32; ::_thesis: verum end; then x,d // a,e2 by A12, A25, DIRAF:3; then x,d // x,y by A48, A29, DIRAF:3; then A53: ( Mid x,d,y or Mid x,y,d ) by DIRAF:7; then A54: Mid d,y,x by A32, DIRAF:9; now__::_thesis:_Mid_c,y,b A55: b <> e2 proof A56: a,b // b,d by A1, DIRAF:def_3; assume A57: b = e2 ; ::_thesis: contradiction c,e1 // x,d by A12, DIRAF:2; then a,b // x,d by A25, A50, A57, ANALOAF:def_5; then x,d // b,d by A5, A56, ANALOAF:def_5; then d,x // d,b by DIRAF:2; then ( Mid d,x,b or Mid d,b,x ) by DIRAF:7; then ( LIN d,x,b or LIN d,b,x ) by DIRAF:28; then A58: LIN d,b,x by DIRAF:30; LIN d,b,b by DIRAF:31; then A59: LIN a,x,b by A7, A14, A58, DIRAF:32; A60: LIN a,x,c by A2, DIRAF:28; LIN a,x,a by A7, A14, A58, DIRAF:32; hence contradiction by A3, A9, A59, A60, DIRAF:32; ::_thesis: verum end; A61: LIN b,d,a by A14, DIRAF:30; A62: y <> d proof A63: LIN c,e2,c by DIRAF:31; A64: LIN c,e2,b by A27, DIRAF:30; assume y = d ; ::_thesis: contradiction then LIN c,d,e2 by A28, DIRAF:28; then LIN c,e2,d by DIRAF:30; then LIN c,e2,a by A7, A14, A64, DIRAF:35; hence contradiction by A3, A31, A64, A63, DIRAF:32; ::_thesis: verum end; A65: LIN b,e2,c by A27, DIRAF:30; assume A66: not Mid c,y,b ; ::_thesis: contradiction then A67: y <> b by DIRAF:10; Mid b,y,e2 by A28, A30, A66, DIRAF:11; then consider z being Element of OAS such that A68: Mid b,d,z and A69: y,d // e2,z by A67, Th20; A70: LIN a,e2,a by DIRAF:31; A71: now__::_thesis:_not_a_=_z assume A72: a = z ; ::_thesis: contradiction Mid d,b,a by A1, DIRAF:9; hence contradiction by A7, A68, A72, DIRAF:14; ::_thesis: verum end; d,y // y,x by A54, DIRAF:def_3; then d,y // d,x by ANALOAF:def_5; then y,d // x,d by DIRAF:2; then y,d // c,e1 by A12, A21, DIRAF:3; then c,e1 // e2,z by A69, A62, ANALOAF:def_5; then a,e2 // e2,z by A25, A50, ANALOAF:def_5; then Mid a,e2,z by DIRAF:def_3; then LIN a,e2,z by DIRAF:28; then A73: LIN a,z,e2 by DIRAF:30; A74: LIN b,d,z by A68, DIRAF:28; then A75: LIN a,z,a by A7, A61, DIRAF:32; LIN b,d,b by DIRAF:31; then LIN a,z,b by A7, A74, A61, DIRAF:32; then A76: LIN a,e2,b by A73, A75, A71, DIRAF:32; LIN a,e2,e2 by A73, A75, A71, DIRAF:32; then LIN a,e2,c by A55, A76, A65, DIRAF:35; hence contradiction by A3, A48, A76, A70, DIRAF:32; ::_thesis: verum end; then Mid b,y,c by DIRAF:9; hence ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) by A53, A32; ::_thesis: verum end; A77: ( b = d implies ( Mid b,d,c & Mid x,d,d ) ) by DIRAF:10; A78: ( x = c implies ( Mid b,c,c & Mid x,c,d ) ) by DIRAF:10; ( a = x implies ( Mid b,b,c & Mid x,b,d ) ) by A1, DIRAF:10; hence ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) by A6, A77, A78; ::_thesis: verum end; theorem :: PASCH:30 for OAS being OAffinSpace holds OAS is satisfying_Int_Bet_Pasch proof let OAS be OAffinSpace; ::_thesis: OAS is satisfying_Int_Bet_Pasch let a be Element of OAS; :: according to PASCH:def_5 ::_thesis: for 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 ) let b, c, d, x, y be Element of OAS; ::_thesis: ( Mid a,b,d & Mid a,x,c & not LIN a,b,c implies ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) ) assume that A1: Mid a,b,d and A2: Mid a,x,c and A3: not LIN a,b,c ; ::_thesis: ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) thus ex y being Element of OAS st ( Mid b,y,c & Mid x,y,d ) by A1, A2, A3, Th29; ::_thesis: verum end; theorem :: PASCH:31 for OAS being OAffinSpace for p, a, b, p9, a9, b9 being Element of OAS st Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & p,p9 // a,a9 & p,p9 // b,b9 holds Mid p9,a9,b9 proof let OAS be OAffinSpace; ::_thesis: for p, a, b, p9, a9, b9 being Element of OAS st Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & p,p9 // a,a9 & p,p9 // b,b9 holds Mid p9,a9,b9 let p, a, b, p9, a9, b9 be Element of OAS; ::_thesis: ( Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & p,p9 // a,a9 & p,p9 // b,b9 implies Mid p9,a9,b9 ) assume that A1: Mid p,a,b and A2: p,a // p9,a9 and A3: not LIN p,a,p9 and A4: LIN p9,a9,b9 and A5: p,p9 // a,a9 and A6: p,p9 // b,b9 ; ::_thesis: Mid p9,a9,b9 A7: p <> a by A3, DIRAF:31; A8: p <> p9 by A3, DIRAF:31; A9: LIN p,a,b by A1, DIRAF:28; then A10: LIN p,b,a by DIRAF:30; now__::_thesis:_(_p9_<>_a9_&_a9_<>_b9_implies_Mid_p9,a9,b9_) A11: p <> b by A1, A7, DIRAF:8; A12: p9 <> b9 proof assume A13: p9 = b9 ; ::_thesis: contradiction then b9,p // b9,b by A6, DIRAF:2; then ( Mid b9,p,b or Mid b9,b,p ) by DIRAF:7; then ( LIN b9,p,b or LIN b9,b,p ) by DIRAF:28; then A14: LIN p,b,b9 by DIRAF:30; LIN p,b,p by DIRAF:31; hence contradiction by A3, A10, A11, A13, A14, DIRAF:32; ::_thesis: verum end; A15: not LIN p,a,a9 proof assume A16: LIN p,a,a9 ; ::_thesis: contradiction p,a '||' a9,p9 by A2, DIRAF:def_4; hence contradiction by A3, A7, A16, DIRAF:33; ::_thesis: verum end; then A17: a <> a9 by DIRAF:31; A18: now__::_thesis:_not_LIN_a,a9,p9 a,a9 // p,p9 by A5, DIRAF:2; then A19: a,a9 '||' p9,p by DIRAF:def_4; assume LIN a,a9,p9 ; ::_thesis: contradiction then LIN a,a9,p by A17, A19, DIRAF:33; hence contradiction by A15, DIRAF:30; ::_thesis: verum end; assume that A20: p9 <> a9 and a9 <> b9 ; ::_thesis: Mid p9,a9,b9 consider x being Element of OAS such that A21: Mid p,x,b9 and A22: b,b9 // a,x by A1, Th19; Mid b9,x,p by A21, DIRAF:9; then consider y being Element of OAS such that A23: Mid b9,y,p9 and A24: p,p9 // x,y by Th19; LIN b9,y,p9 by A23, DIRAF:28; then A25: LIN p9,b9,y by DIRAF:30; A26: b <> b9 proof assume b = b9 ; ::_thesis: contradiction then LIN a9,p9,b by A4, DIRAF:30; then a9,p9 '||' a9,b by DIRAF:def_5; then ( a9,p9 // a9,b or a9,p9 // b,a9 ) by DIRAF:def_4; then ( p9,a9 // a9,b or p9,a9 // b,a9 ) by DIRAF:2; then ( p,a // a9,b or p,a // b,a9 ) by A2, A20, DIRAF:3; then p,a '||' b,a9 by DIRAF:def_4; hence contradiction by A1, A7, A15, DIRAF:28, DIRAF:33; ::_thesis: verum end; A27: x <> a proof assume x = a ; ::_thesis: contradiction then A28: LIN p,a,b9 by A21, DIRAF:28; LIN p,a,a by DIRAF:31; then A29: LIN b,b9,a by A7, A9, A28, DIRAF:32; LIN p,a,p by DIRAF:31; then A30: LIN b,b9,p by A7, A9, A28, DIRAF:32; b,b9 // p,p9 by A6, DIRAF:2; then b,b9 '||' p,p9 by DIRAF:def_4; then LIN b,b9,p9 by A26, A30, DIRAF:33; hence contradiction by A3, A26, A29, A30, DIRAF:32; ::_thesis: verum end; A31: LIN p9,b9,a9 by A4, DIRAF:30; then A32: LIN y,a9,a9 by A12, A25, DIRAF:32; A33: p,p9 // a,x by A6, A22, A26, DIRAF:3; then a,x // x,y by A8, A24, ANALOAF:def_5; then a,x // a,y by ANALOAF:def_5; then p,p9 // a,y by A27, A33, DIRAF:3; then a,y // a,a9 by A5, A8, ANALOAF:def_5; then a,y '||' a,a9 by DIRAF:def_4; then LIN a,y,a9 by DIRAF:def_5; then A34: LIN y,a9,a by DIRAF:30; LIN p9,b9,p9 by DIRAF:31; then LIN y,a9,p9 by A12, A25, A31, DIRAF:32; then ( y = a9 or LIN a,a9,p9 ) by A34, A32, DIRAF:32; hence Mid p9,a9,b9 by A23, A18, DIRAF:9; ::_thesis: verum end; hence Mid p9,a9,b9 by DIRAF:10; ::_thesis: verum end;