:: SEMI_AF1 semantic presentation begin definition let IT be non empty AffinStruct ; attrIT is Semi_Affine_Space-like means :Def1: :: SEMI_AF1:def 1 ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st ( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st for b, c being Element of IT holds ( o,a // o,p & ex d being Element of IT st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ); end; :: deftheorem Def1 defines Semi_Affine_Space-like SEMI_AF1:def_1_:_ for IT being non empty AffinStruct holds ( IT is Semi_Affine_Space-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st ( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st for b, c being Element of IT holds ( o,a // o,p & ex d being Element of IT st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) ); registration cluster non empty Semi_Affine_Space-like for AffinStruct ; existence ex b1 being non empty AffinStruct st b1 is Semi_Affine_Space-like proof consider SAS being AffinPlane such that A1: ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) by PARDEPAP:4; reconsider AS = SAS as non empty AffinStruct ; take AS ; ::_thesis: AS is Semi_Affine_Space-like thus for a, b being Element of AS holds a,b // b,a by DIRAF:40; :: according to SEMI_AF1:def_1 ::_thesis: ( ( for a, b, c being Element of AS holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of AS st a <> b & a,b // p,q & a,b // r,s holds p,q // r,s ) & ( for a, b, c being Element of AS st a,b // a,c holds b,a // b,c ) & not for a, b, c being Element of AS holds a,b // a,c & ( for a, b, p being Element of AS ex q being Element of AS st ( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of AS ex p being Element of AS st for b, c being Element of AS holds ( o,a // o,p & ex d being Element of AS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of AS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of AS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of AS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of AS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) thus ( ( for a, b, c being Element of AS holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of AS st a <> b & a,b // p,q & a,b // r,s holds p,q // r,s ) & ( for a, b, c being Element of AS st a,b // a,c holds b,a // b,c ) & not for a, b, c being Element of AS holds a,b // a,c & ( for a, b, p being Element of AS ex q being Element of AS st ( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of AS ex p being Element of AS st for b, c being Element of AS holds ( o,a // o,p & ex d being Element of AS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a9, b, b9, c, c9 being Element of AS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of AS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of AS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of AS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) by A1, DIRAF:40, PARDEPAP:5; ::_thesis: verum end; end; definition mode Semi_Affine_Space is non empty Semi_Affine_Space-like AffinStruct ; end; theorem Th1: :: SEMI_AF1:1 for SAS being Semi_Affine_Space for a, b being Element of SAS holds a,b // a,b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b being Element of SAS holds a,b // a,b let a, b be Element of SAS; ::_thesis: a,b // a,b b,a // b,b by Def1; hence a,b // a,b by Def1; ::_thesis: verum end; theorem Th2: :: SEMI_AF1:2 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a,b // c,d holds c,d // a,b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a,b // c,d holds c,d // a,b let a, b, c, d be Element of SAS; ::_thesis: ( a,b // c,d implies c,d // a,b ) assume A1: a,b // c,d ; ::_thesis: c,d // a,b a,b // a,b by Th1; then ( a <> b implies c,d // a,b ) by A1, Def1; hence c,d // a,b by Def1; ::_thesis: verum end; theorem Th3: :: SEMI_AF1:3 for SAS being Semi_Affine_Space for a, b, c being Element of SAS holds a,a // b,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS holds a,a // b,c let a, b, c be Element of SAS; ::_thesis: a,a // b,c b,c // a,a by Def1; hence a,a // b,c by Th2; ::_thesis: verum end; theorem Th4: :: SEMI_AF1:4 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a,b // c,d holds b,a // c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a,b // c,d holds b,a // c,d let a, b, c, d be Element of SAS; ::_thesis: ( a,b // c,d implies b,a // c,d ) assume A1: a,b // c,d ; ::_thesis: b,a // c,d a,b // b,a by Def1; then ( a <> b implies b,a // c,d ) by A1, Def1; hence b,a // c,d by A1; ::_thesis: verum end; theorem Th5: :: SEMI_AF1:5 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a,b // c,d holds a,b // d,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a,b // c,d holds a,b // d,c let a, b, c, d be Element of SAS; ::_thesis: ( a,b // c,d implies a,b // d,c ) assume a,b // c,d ; ::_thesis: a,b // d,c then c,d // a,b by Th2; then d,c // a,b by Th4; hence a,b // d,c by Th2; ::_thesis: verum end; theorem Th6: :: SEMI_AF1:6 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a,b // c,d holds ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a,b // c,d holds ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) let a, b, c, d be Element of SAS; ::_thesis: ( a,b // c,d implies ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) ) assume a,b // c,d ; ::_thesis: ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) then c,d // a,b by Th2; then A1: d,c // a,b by Th4; then A2: d,c // b,a by Th5; then c,d // b,a by Th4; hence ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) by A1, A2, Th2, Th4; ::_thesis: verum end; theorem Th7: :: SEMI_AF1:7 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st a,b // a,c holds ( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st a,b // a,c holds ( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c ) let a, b, c be Element of SAS; ::_thesis: ( a,b // a,c implies ( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c ) ) assume A1: a,b // a,c ; ::_thesis: ( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c ) then a,c // a,b by Th2; then A2: c,a // c,b by Def1; b,a // b,c by A1, Def1; hence ( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c ) by A1, A2, Th6; ::_thesis: verum end; theorem Th8: :: SEMI_AF1:8 for SAS being Semi_Affine_Space for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds p,q // r,s proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds p,q // r,s let a, b, p, q, r, s be Element of SAS; ::_thesis: ( a <> b & p,q // a,b & a,b // r,s implies p,q // r,s ) assume that A1: a <> b and A2: p,q // a,b and A3: a,b // r,s ; ::_thesis: p,q // r,s a,b // p,q by A2, Th6; hence p,q // r,s by A1, A3, Def1; ::_thesis: verum end; theorem :: SEMI_AF1:9 for SAS being Semi_Affine_Space for a, b, d being Element of SAS st not a,b // a,d holds ( a <> b & b <> d & d <> a ) by Def1, Th1, Th3; theorem :: SEMI_AF1:10 for SAS being Semi_Affine_Space for a, b, p, q being Element of SAS st not a,b // p,q holds ( a <> b & p <> q ) by Def1, Th3; theorem :: SEMI_AF1:11 for SAS being Semi_Affine_Space for a, b, x, c being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds a,b // a,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, x, c being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds a,b // a,c let a, b, x, c be Element of SAS; ::_thesis: ( a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c ) assume that A1: a,b // a,x and A2: b,c // b,x and A3: c,a // c,x ; ::_thesis: a,b // a,c now__::_thesis:_(_a_<>_x_implies_a,b_//_a,c_) assume A4: a <> x ; ::_thesis: a,b // a,c ( a,x // a,b & a,x // a,c ) by A1, A3, Th7; hence a,b // a,c by A4, Def1; ::_thesis: verum end; hence a,b // a,c by A2, Th7; ::_thesis: verum end; theorem Th12: :: SEMI_AF1:12 for SAS being Semi_Affine_Space for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds not p,q // p,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds not p,q // p,c let a, b, c, p, q be Element of SAS; ::_thesis: ( not a,b // a,c & p <> q & p,q // p,a & p,q // p,b implies not p,q // p,c ) assume that A1: not a,b // a,c and A2: p <> q ; ::_thesis: ( not p,q // p,a or not p,q // p,b or not p,q // p,c ) now__::_thesis:_(_a_<>_p_&_p,q_//_p,a_&_p,q_//_p,b_implies_not_p,q_//_p,c_) assume that A3: a <> p and A4: p,q // p,a and A5: p,q // p,b and A6: p,q // p,c ; ::_thesis: contradiction p,a // p,c by A2, A4, A6, Def1; then A7: a,p // a,c by Def1; p,a // p,b by A2, A4, A5, Def1; then a,p // a,b by Def1; hence contradiction by A1, A3, A7, Def1; ::_thesis: verum end; hence ( not p,q // p,a or not p,q // p,b or not p,q // p,c ) by A1, A2, Def1; ::_thesis: verum end; theorem Th13: :: SEMI_AF1:13 for SAS being Semi_Affine_Space for p, q being Element of SAS st p <> q holds ex r being Element of SAS st not p,q // p,r proof let SAS be Semi_Affine_Space; ::_thesis: for p, q being Element of SAS st p <> q holds ex r being Element of SAS st not p,q // p,r let p, q be Element of SAS; ::_thesis: ( p <> q implies ex r being Element of SAS st not p,q // p,r ) consider a, b, c being Element of SAS such that A1: not a,b // a,c by Def1; assume p <> q ; ::_thesis: not for r being Element of SAS holds p,q // p,r then ( not p,q // p,a or not p,q // p,b or not p,q // p,c ) by A1, Th12; hence not for r being Element of SAS holds p,q // p,r ; ::_thesis: verum end; theorem Th14: :: SEMI_AF1:14 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st not a,b // a,c holds ( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st not a,b // a,c holds ( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b ) let a, b, c be Element of SAS; ::_thesis: ( not a,b // a,c implies ( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b ) ) assume A1: not a,b // a,c ; ::_thesis: ( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b ) A2: now__::_thesis:_not_a,c_//_c,b assume a,c // c,b ; ::_thesis: contradiction then c,a // c,b by Th6; hence contradiction by A1, Th7; ::_thesis: verum end; assume A3: ( a,b // c,a or b,a // a,c or b,a // c,a or a,c // a,b or a,c // b,a or c,a // a,b or c,a // b,a or b,a // b,c or b,a // c,b or a,b // b,c or a,b // c,b or b,c // b,a or b,c // a,b or c,b // a,b or c,b // b,a or c,b // c,a or c,b // a,c or b,c // c,a or b,c // a,c or c,a // c,b or c,a // b,c or a,c // b,c or a,c // c,b ) ; ::_thesis: contradiction not b,a // b,c by A1, Th7; hence contradiction by A1, A3, A2, Th6; ::_thesis: verum end; theorem Th15: :: SEMI_AF1:15 for SAS being Semi_Affine_Space for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds not p,q // r,s proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds not p,q // r,s let a, b, c, d, p, q, r, s be Element of SAS; ::_thesis: ( not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s implies not p,q // r,s ) assume that A1: not a,b // c,d and A2: a,b // p,q and A3: c,d // r,s and A4: p <> q and A5: r <> s ; ::_thesis: not p,q // r,s assume p,q // r,s ; ::_thesis: contradiction then a,b // r,s by A2, A4, Th8; then A6: r,s // a,b by Th6; r,s // c,d by A3, Th6; hence contradiction by A1, A5, A6, Def1; ::_thesis: verum end; theorem Th16: :: SEMI_AF1:16 for SAS being Semi_Affine_Space for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds not p,q // p,r proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds not p,q // p,r let a, b, c, p, q, r be Element of SAS; ::_thesis: ( not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q implies not p,q // p,r ) assume that A1: not a,b // a,c and A2: a,b // p,q and A3: a,c // p,r and A4: b,c // q,r and A5: p <> q ; ::_thesis: not p,q // p,r now__::_thesis:_not_p_=_r assume p = r ; ::_thesis: contradiction then A6: p,q // b,c by A4, Th6; p,q // a,b by A2, Th6; then a,b // b,c by A5, A6, Def1; then b,a // b,c by Th4; hence contradiction by A1, Th7; ::_thesis: verum end; hence not p,q // p,r by A1, A2, A3, A5, Th15; ::_thesis: verum end; theorem Th17: :: SEMI_AF1:17 for SAS being Semi_Affine_Space for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds p = r proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds p = r let a, b, c, p, r be Element of SAS; ::_thesis: ( not a,b // a,c & a,c // p,r & b,c // p,r implies p = r ) assume that A1: ( not a,b // a,c & a,c // p,r ) and A2: b,c // p,r ; ::_thesis: p = r A3: p,r // b,c by A2, Th6; ( not a,c // b,c & p,r // a,c ) by A1, Th6, Th14; hence p = r by A3, Def1; ::_thesis: verum end; theorem Th18: :: SEMI_AF1:18 for SAS being Semi_Affine_Space for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds r1 = r2 proof let SAS be Semi_Affine_Space; ::_thesis: for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds r1 = r2 let p, q, r1, r2 be Element of SAS; ::_thesis: ( not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1 = r2 ) assume that A1: ( not p,q // p,r1 & p,r1 // p,r2 ) and A2: q,r1 // q,r2 ; ::_thesis: r1 = r2 A3: r1,r2 // r1,q by A2, Th14; ( not r1,p // r1,q & r1,r2 // r1,p ) by A1, Th14; hence r1 = r2 by A3, Def1; ::_thesis: verum end; theorem Th19: :: SEMI_AF1:19 for SAS being Semi_Affine_Space for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds r1 = r2 proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds r1 = r2 let a, b, c, p, q, r1, r2 be Element of SAS; ::_thesis: ( not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 implies r1 = r2 ) assume that A1: not a,b // a,c and A2: a,b // p,q and A3: a,c // p,r1 and A4: a,c // p,r2 and A5: b,c // q,r1 and A6: b,c // q,r2 ; ::_thesis: r1 = r2 A7: now__::_thesis:_(_p_<>_q_implies_r1_=_r2_) b <> c by A1, Th1; then A8: q,r1 // q,r2 by A5, A6, Def1; a <> c by A1, Def1; then A9: p,r1 // p,r2 by A3, A4, Def1; assume p <> q ; ::_thesis: r1 = r2 then not p,q // p,r1 by A1, A2, A3, A5, Th16; hence r1 = r2 by A9, A8, Th18; ::_thesis: verum end; now__::_thesis:_(_p_=_q_implies_r1_=_r2_) assume A10: p = q ; ::_thesis: r1 = r2 then p = r1 by A1, A3, A5, Th17; hence r1 = r2 by A1, A4, A6, A10, Th17; ::_thesis: verum end; hence r1 = r2 by A7; ::_thesis: verum end; theorem :: SEMI_AF1:20 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds a,b // c,d by Def1, Th1, Th3; theorem :: SEMI_AF1:21 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st ( a = b or a = c or b = c ) holds a,b // a,c by Def1, Th1, Th3; definition let SAS be Semi_Affine_Space; let a, b, c be Element of SAS; preda,b,c is_collinear means :Def2: :: SEMI_AF1:def 2 a,b // a,c; end; :: deftheorem Def2 defines is_collinear SEMI_AF1:def_2_:_ for SAS being Semi_Affine_Space for a, b, c being Element of SAS holds ( a,b,c is_collinear iff a,b // a,c ); theorem Th22: :: SEMI_AF1:22 for SAS being Semi_Affine_Space for a1, a2, a3 being Element of SAS st a1,a2,a3 is_collinear holds ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) proof let SAS be Semi_Affine_Space; ::_thesis: for a1, a2, a3 being Element of SAS st a1,a2,a3 is_collinear holds ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) let a1, a2, a3 be Element of SAS; ::_thesis: ( a1,a2,a3 is_collinear implies ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) ) assume a1,a2,a3 is_collinear ; ::_thesis: ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) then A1: a1,a2 // a1,a3 by Def2; then A2: ( a2,a3 // a2,a1 & a3,a2 // a3,a1 ) by Th7; A3: a3,a1 // a3,a2 by A1, Th7; ( a1,a3 // a1,a2 & a2,a1 // a2,a3 ) by A1, Th7; hence ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) by A2, A3, Def2; ::_thesis: verum end; theorem Th23: :: SEMI_AF1:23 for SAS being Semi_Affine_Space for a, b, c, p, q, r being Element of SAS st not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds not p,q,r is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, p, q, r being Element of SAS st not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds not p,q,r is_collinear let a, b, c, p, q, r be Element of SAS; ::_thesis: ( not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r implies not p,q,r is_collinear ) assume that A1: not a,b,c is_collinear and A2: ( a,b // p,q & a,c // p,r & p <> q & p <> r ) ; ::_thesis: not p,q,r is_collinear not a,b // a,c by A1, Def2; then not p,q // p,r by A2, Th15; hence not p,q,r is_collinear by Def2; ::_thesis: verum end; theorem Th24: :: SEMI_AF1:24 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds a,b,c is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds a,b,c is_collinear let a, b, c be Element of SAS; ::_thesis: ( ( a = b or b = c or c = a ) implies a,b,c is_collinear ) assume ( a = b or b = c or c = a ) ; ::_thesis: a,b,c is_collinear then a,b // a,c by Def1, Th1, Th3; hence a,b,c is_collinear by Def2; ::_thesis: verum end; theorem Th25: :: SEMI_AF1:25 for SAS being Semi_Affine_Space for p, q being Element of SAS st p <> q holds ex r being Element of SAS st not p,q,r is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for p, q being Element of SAS st p <> q holds ex r being Element of SAS st not p,q,r is_collinear let p, q be Element of SAS; ::_thesis: ( p <> q implies ex r being Element of SAS st not p,q,r is_collinear ) assume p <> q ; ::_thesis: not for r being Element of SAS holds p,q,r is_collinear then consider r being Element of SAS such that A1: not p,q // p,r by Th13; take r ; ::_thesis: not p,q,r is_collinear thus not p,q,r is_collinear by A1, Def2; ::_thesis: verum end; theorem Th26: :: SEMI_AF1:26 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a,b,c is_collinear & a,b,d is_collinear holds a,b // c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a,b,c is_collinear & a,b,d is_collinear holds a,b // c,d let a, b, c, d be Element of SAS; ::_thesis: ( a,b,c is_collinear & a,b,d is_collinear implies a,b // c,d ) assume that A1: a,b,c is_collinear and A2: a,b,d is_collinear ; ::_thesis: a,b // c,d now__::_thesis:_(_a_<>_b_&_a_<>_c_implies_a,b_//_c,d_) assume that A3: a <> b and A4: a <> c ; ::_thesis: a,b // c,d A5: a,b // a,c by A1, Def2; a,b // a,d by A2, Def2; then a,c // a,d by A3, A5, Def1; then a,c // c,d by Th7; hence a,b // c,d by A4, A5, Th8; ::_thesis: verum end; hence a,b // c,d by A2, Def2, Th3; ::_thesis: verum end; theorem Th27: :: SEMI_AF1:27 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st not a,b,c is_collinear & a,b // c,d holds not a,b,d is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st not a,b,c is_collinear & a,b // c,d holds not a,b,d is_collinear let a, b, c, d be Element of SAS; ::_thesis: ( not a,b,c is_collinear & a,b // c,d implies not a,b,d is_collinear ) assume that A1: not a,b,c is_collinear and A2: a,b // c,d ; ::_thesis: not a,b,d is_collinear now__::_thesis:_(_c_<>_d_implies_not_a,b,d_is_collinear_) assume that A3: c <> d and A4: a,b,d is_collinear ; ::_thesis: contradiction a,b // a,d by A4, Def2; then A5: a,b // d,a by Th6; A6: a,b // d,c by A2, Th6; A7: a,c // c,a by Def1; A8: not a,b // a,c by A1, Def2; then a <> b by Th3; then A9: d,c // d,a by A6, A5, Def1; c <> a by A8, Def1; then not c,d // c,a by A2, A3, A8, A7, Th15; hence contradiction by A9, Th7; ::_thesis: verum end; hence not a,b,d is_collinear by A1; ::_thesis: verum end; theorem Th28: :: SEMI_AF1:28 for SAS being Semi_Affine_Space for a, b, c, d, x being Element of SAS st not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear holds not a,b,x is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, x being Element of SAS st not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear holds not a,b,x is_collinear let a, b, c, d, x be Element of SAS; ::_thesis: ( not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear implies not a,b,x is_collinear ) assume that A1: ( not a,b,c is_collinear & a,b // c,d & c <> d ) and A2: c,d,x is_collinear ; ::_thesis: not a,b,x is_collinear c,d // c,x by A2, Def2; hence not a,b,x is_collinear by A1, Th8, Th27; ::_thesis: verum end; theorem :: SEMI_AF1:29 for SAS being Semi_Affine_Space for o, a, b, x being Element of SAS st not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear holds o = x proof let SAS be Semi_Affine_Space; ::_thesis: for o, a, b, x being Element of SAS st not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear holds o = x let o, a, b, x be Element of SAS; ::_thesis: ( not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear implies o = x ) assume that A1: not o,a,b is_collinear and A2: o,a,x is_collinear and A3: o,b,x is_collinear ; ::_thesis: o = x b,o,x is_collinear by A3, Th22; then A4: b,o // b,x by Def2; o,a // o,x by A2, Def2; then A5: a,o // a,x by Th14; not a,b,o is_collinear by A1, Th22; then not a,b // a,o by Def2; hence o = x by A5, A4, Th18; ::_thesis: verum end; theorem :: SEMI_AF1:30 for SAS being Semi_Affine_Space for o, a, b, a9, b9 being Element of SAS st o <> a & o <> b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear holds a,b // a9,b9 proof let SAS be Semi_Affine_Space; ::_thesis: for o, a, b, a9, b9 being Element of SAS st o <> a & o <> b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear holds a,b // a9,b9 let o, a, b, a9, b9 be Element of SAS; ::_thesis: ( o <> a & o <> b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear implies a,b // a9,b9 ) assume that A1: o <> a and A2: o <> b and A3: o,a,b is_collinear and A4: o,a,a9 is_collinear and A5: o,b,b9 is_collinear ; ::_thesis: a,b // a9,b9 A6: now__::_thesis:_(_o_<>_a9_implies_a,b_//_a9,b9_) A7: o,a // o,b by A3, Def2; o,a // o,a9 by A4, Def2; then A8: o,b // o,a9 by A1, A7, Def1; o,b // o,b9 by A5, Def2; then o,a9 // o,b9 by A2, A8, Def1; then A9: o,a9 // a9,b9 by Th7; o,b // a,b by A7, Th7; then A10: a,b // o,a9 by A2, A8, Def1; assume o <> a9 ; ::_thesis: a,b // a9,b9 hence a,b // a9,b9 by A10, A9, Th8; ::_thesis: verum end; now__::_thesis:_(_o_=_a9_implies_a,b_//_a9,b9_) assume A11: o = a9 ; ::_thesis: a,b // a9,b9 then a9,a // a9,b by A3, Def2; then A12: a,b // a9,b by Th7; a9,b // a9,b9 by A5, A11, Def2; hence a,b // a9,b9 by A2, A11, A12, Th8; ::_thesis: verum end; hence a,b // a9,b9 by A6; ::_thesis: verum end; theorem :: SEMI_AF1:31 for SAS being Semi_Affine_Space for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1 is_collinear & c,d,p2 is_collinear holds p1 = p2 proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1 is_collinear & c,d,p2 is_collinear holds p1 = p2 let a, b, c, d, p1, p2 be Element of SAS; ::_thesis: ( not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1 is_collinear & c,d,p2 is_collinear implies p1 = p2 ) assume that A1: not a,b // c,d and A2: ( a,b,p1 is_collinear & a,b,p2 is_collinear ) and A3: ( c,d,p1 is_collinear & c,d,p2 is_collinear ) ; ::_thesis: p1 = p2 c,d // p1,p2 by A3, Th26; then A4: p1,p2 // c,d by Th6; a,b // p1,p2 by A2, Th26; then p1,p2 // a,b by Th6; hence p1 = p2 by A1, A4, Def1; ::_thesis: verum end; theorem Th32: :: SEMI_AF1:32 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds a,c // b,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds a,c // b,d let a, b, c, d be Element of SAS; ::_thesis: ( a <> b & a,b,c is_collinear & a,b // c,d implies a,c // b,d ) assume that A1: a <> b and A2: a,b,c is_collinear and A3: a,b // c,d ; ::_thesis: a,c // b,d now__::_thesis:_(_b_<>_c_implies_a,c_//_b,d_) A4: a,b // a,c by A2, Def2; then a,b // c,b by Th7; then c,b // c,d by A1, A3, Def1; then A5: b,c // b,d by Th7; assume A6: b <> c ; ::_thesis: a,c // b,d b,c // a,c by A4, Th7; hence a,c // b,d by A6, A5, Def1; ::_thesis: verum end; hence a,c // b,d by A3; ::_thesis: verum end; theorem Th33: :: SEMI_AF1:33 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds c,b // c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds c,b // c,d let a, b, c, d be Element of SAS; ::_thesis: ( a <> b & a,b,c is_collinear & a,b // c,d implies c,b // c,d ) assume that A1: a <> b and A2: a,b,c is_collinear and A3: a,b // c,d ; ::_thesis: c,b // c,d now__::_thesis:_(_a_<>_c_implies_c,b_//_c,d_) a,b // a,c by A2, Def2; then A4: ( a,c // c,b & a,c // c,d ) by A1, A3, Def1, Th7; assume a <> c ; ::_thesis: c,b // c,d hence c,b // c,d by A4, Def1; ::_thesis: verum end; hence c,b // c,d by A3; ::_thesis: verum end; theorem Th34: :: SEMI_AF1:34 for SAS being Semi_Affine_Space for o, a, c, b, d1, d2 being Element of SAS st not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 holds d1 = d2 proof let SAS be Semi_Affine_Space; ::_thesis: for o, a, c, b, d1, d2 being Element of SAS st not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 holds d1 = d2 let o, a, c, b, d1, d2 be Element of SAS; ::_thesis: ( not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 implies d1 = d2 ) assume that A1: ( not o,a,c is_collinear & o,a,b is_collinear ) and A2: ( o,c,d1 is_collinear & o,c,d2 is_collinear ) and A3: ( a,c // b,d1 & a,c // b,d2 ) ; ::_thesis: d1 = d2 A4: ( o,c // o,d1 & o,c // o,d2 ) by A2, Def2; ( not o,a // o,c & o,a // o,b ) by A1, Def2; hence d1 = d2 by A3, A4, Th19; ::_thesis: verum end; theorem :: SEMI_AF1:35 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear let a, b, c, d be Element of SAS; ::_thesis: ( a <> b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear ) assume that A1: a <> b and A2: ( a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,c,d is_collinear ( a,b // a,c & a,b // a,d ) by A2, Def2; then a,c // a,d by A1, Def1; hence a,c,d is_collinear by Def2; ::_thesis: verum end; definition let SAS be Semi_Affine_Space; let a, b, c, d be Element of SAS; pred parallelogram a,b,c,d means :Def3: :: SEMI_AF1:def 3 ( not a,b,c is_collinear & a,b // c,d & a,c // b,d ); end; :: deftheorem Def3 defines parallelogram SEMI_AF1:def_3_:_ for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS holds ( parallelogram a,b,c,d iff ( not a,b,c is_collinear & a,b // c,d & a,c // b,d ) ); theorem Th36: :: SEMI_AF1:36 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d ) let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d ) ) assume A1: parallelogram a,b,c,d ; ::_thesis: ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d ) then not a,b,c is_collinear by Def3; hence ( a <> b & a <> c & c <> b ) by Th24; ::_thesis: ( a <> d & b <> d & c <> d ) A2: now__::_thesis:_not_a_=_d assume a = d ; ::_thesis: contradiction then a,b // c,a by A1, Def3; then A3: a,b // a,c by Th6; not a,b,c is_collinear by A1, Def3; hence contradiction by A3, Def2; ::_thesis: verum end; A4: now__::_thesis:_not_c_=_d assume c = d ; ::_thesis: contradiction then a,c // b,c by A1, Def3; then c,a // c,b by Th6; then A5: c,a,b is_collinear by Def2; not a,b,c is_collinear by A1, Def3; hence contradiction by A5, Th22; ::_thesis: verum end; A6: now__::_thesis:_not_b_=_d assume b = d ; ::_thesis: contradiction then a,b // c,b by A1, Def3; then b,a // b,c by Th6; then A7: b,a,c is_collinear by Def2; not a,b,c is_collinear by A1, Def3; hence contradiction by A7, Th22; ::_thesis: verum end; assume ( not a <> d or not b <> d or not c <> d ) ; ::_thesis: contradiction hence contradiction by A2, A6, A4; ::_thesis: verum end; theorem Th37: :: SEMI_AF1:37 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) ) A1: a,b // b,a by Def1; assume A2: parallelogram a,b,c,d ; ::_thesis: ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) hence not a,b,c is_collinear by Def3; ::_thesis: ( not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) A3: ( b <> a & b <> d ) by A2, Th36; a,c // b,d by A2, Def3; then A4: a,c // d,b by Th6; a,b // c,d by A2, Def3; then A5: a,b // d,c by Th6; ( not a,b,c is_collinear & a,c // b,d ) by A2, Def3; hence not b,a,d is_collinear by A1, A3, Th23; ::_thesis: ( not c,d,a is_collinear & not d,c,b is_collinear ) A6: a,c // c,a by Def1; A7: ( c <> d & c <> a ) by A2, Th36; ( not a,b,c is_collinear & a,b // c,d ) by A2, Def3; hence not c,d,a is_collinear by A6, A7, Th23; ::_thesis: not d,c,b is_collinear A8: d <> b by A2, Th36; ( not a,b,c is_collinear & c <> d ) by A2, Def3, Th36; hence not d,c,b is_collinear by A5, A4, A8, Th23; ::_thesis: verum end; theorem Th38: :: SEMI_AF1:38 for SAS being Semi_Affine_Space for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) proof let SAS be Semi_Affine_Space; ::_thesis: for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) let a1, a2, a3, a4 be Element of SAS; ::_thesis: ( parallelogram a1,a2,a3,a4 implies ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) ) assume A1: parallelogram a1,a2,a3,a4 ; ::_thesis: ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) then A2: ( not a3,a4,a1 is_collinear & not a4,a3,a2 is_collinear ) by Th37; ( not a1,a2,a3 is_collinear & not a2,a1,a4 is_collinear ) by A1, Th37; hence ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) by A2, Th22; ::_thesis: verum end; theorem Th39: :: SEMI_AF1:39 for SAS being Semi_Affine_Space for a, b, c, d, x being Element of SAS holds ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, x being Element of SAS holds ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear ) let a, b, c, d, x be Element of SAS; ::_thesis: ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear ) assume A1: parallelogram a,b,c,d ; ::_thesis: ( not a,b,x is_collinear or not c,d,x is_collinear ) then A2: c <> d by Th36; ( not a,b,c is_collinear & a,b // c,d ) by A1, Def3; hence ( not a,b,x is_collinear or not c,d,x is_collinear ) by A2, Th28; ::_thesis: verum end; theorem :: SEMI_AF1:40 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram a,c,b,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram a,c,b,d let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies parallelogram a,c,b,d ) assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram a,c,b,d then A2: a,c // b,d by Def3; ( not a,c,b is_collinear & a,b // c,d ) by A1, Def3, Th38; hence parallelogram a,c,b,d by A2, Def3; ::_thesis: verum end; theorem :: SEMI_AF1:41 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram c,d,a,b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram c,d,a,b let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies parallelogram c,d,a,b ) assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram c,d,a,b then a,b // c,d by Def3; then A2: c,d // a,b by Th6; a,c // b,d by A1, Def3; then A3: c,a // d,b by Th6; not c,d,a is_collinear by A1, Th38; hence parallelogram c,d,a,b by A2, A3, Def3; ::_thesis: verum end; theorem :: SEMI_AF1:42 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram b,a,d,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds parallelogram b,a,d,c let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies parallelogram b,a,d,c ) assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram b,a,d,c then a,b // c,d by Def3; then A2: b,a // d,c by Th6; a,c // b,d by A1, Def3; then A3: b,d // a,c by Th6; not b,a,d is_collinear by A1, Th38; hence parallelogram b,a,d,c by A2, A3, Def3; ::_thesis: verum end; theorem Th43: :: SEMI_AF1:43 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) ) assume A1: parallelogram a,b,c,d ; ::_thesis: ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) then A2: ( not c,d,a is_collinear & not b,a,d is_collinear ) by Th38; A3: ( not a,c,b is_collinear & a,c // b,d ) by A1, Def3, Th38; A4: ( not c,a,d is_collinear & not d,b,c is_collinear ) by A1, Th38; A5: a,b // c,d by A1, Def3; then A6: d,c // b,a by Th6; A7: a,c // b,d by A1, Def3; then A8: ( c,a // d,b & b,d // a,c ) by Th6; A9: not b,d,a is_collinear by A1, Th38; A10: d,b // c,a by A7, Th6; ( c,d // a,b & b,a // d,c ) by A5, Th6; hence ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) by A5, A3, A2, A8, A4, A10, A6, A9, Def3; ::_thesis: verum end; theorem Th44: :: SEMI_AF1:44 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st not a,b,c is_collinear holds ex d being Element of SAS st parallelogram a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st not a,b,c is_collinear holds ex d being Element of SAS st parallelogram a,b,c,d let a, b, c be Element of SAS; ::_thesis: ( not a,b,c is_collinear implies ex d being Element of SAS st parallelogram a,b,c,d ) assume A1: not a,b,c is_collinear ; ::_thesis: ex d being Element of SAS st parallelogram a,b,c,d consider d being Element of SAS such that A2: ( a,b // c,d & a,c // b,d ) by Def1; take d ; ::_thesis: parallelogram a,b,c,d thus parallelogram a,b,c,d by A1, A2, Def3; ::_thesis: verum end; theorem Th45: :: SEMI_AF1:45 for SAS being Semi_Affine_Space for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds d1 = d2 proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds d1 = d2 let a, b, c, d1, d2 be Element of SAS; ::_thesis: ( parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1 = d2 ) assume that A1: parallelogram a,b,c,d1 and A2: parallelogram a,b,c,d2 ; ::_thesis: d1 = d2 not b,c,a is_collinear by A1, Th38; then A3: not b,c // b,a by Def2; a,c // b,d2 by A2, Def3; then A4: c,a // b,d2 by Th6; a,b // c,d2 by A2, Def3; then A5: b,a // c,d2 by Th6; a,c // b,d1 by A1, Def3; then A6: c,a // b,d1 by Th6; a,b // c,d1 by A1, Def3; then A7: b,a // c,d1 by Th6; b,c // c,b by Def1; hence d1 = d2 by A3, A7, A5, A6, A4, Th19; ::_thesis: verum end; theorem Th46: :: SEMI_AF1:46 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds not a,d // b,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds not a,d // b,c let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies not a,d // b,c ) assume A1: parallelogram a,b,c,d ; ::_thesis: not a,d // b,c then not a,b,c is_collinear by Def3; then A2: not a,b // a,c by Def2; ( a,b // c,d & a,c // b,d ) by A1, Def3; hence not a,d // b,c by A2, Def1; ::_thesis: verum end; theorem Th47: :: SEMI_AF1:47 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds not parallelogram a,b,d,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds not parallelogram a,b,d,c let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies not parallelogram a,b,d,c ) assume A1: parallelogram a,b,c,d ; ::_thesis: not parallelogram a,b,d,c then not a,b,c is_collinear by Def3; then A2: not a,b // a,c by Def2; assume parallelogram a,b,d,c ; ::_thesis: contradiction then A3: a,d // b,c by Def3; ( a,b // c,d & a,c // b,d ) by A1, Def3; hence contradiction by A3, A2, Def1; ::_thesis: verum end; theorem Th48: :: SEMI_AF1:48 for SAS being Semi_Affine_Space for a, b being Element of SAS st a <> b holds ex c being Element of SAS st ( a,b,c is_collinear & c <> a & c <> b ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b being Element of SAS st a <> b holds ex c being Element of SAS st ( a,b,c is_collinear & c <> a & c <> b ) let a, b be Element of SAS; ::_thesis: ( a <> b implies ex c being Element of SAS st ( a,b,c is_collinear & c <> a & c <> b ) ) assume a <> b ; ::_thesis: ex c being Element of SAS st ( a,b,c is_collinear & c <> a & c <> b ) then consider p being Element of SAS such that A1: not a,b,p is_collinear by Th25; consider q being Element of SAS such that A2: parallelogram a,b,p,q by A1, Th44; not p,q,b is_collinear by A2, Th38; then consider c being Element of SAS such that A3: parallelogram p,q,b,c by Th44; take c ; ::_thesis: ( a,b,c is_collinear & c <> a & c <> b ) A4: p,q // b,c by A3, Def3; ( p <> q & a,b // p,q ) by A2, Def3, Th36; then a,b // b,c by A4, Th8; then b,a // b,c by Th6; then A5: b,a,c is_collinear by Def2; A6: not a,q // b,p by A2, Th46; ( p,b // q,c & not b,c,p is_collinear ) by A3, Def3, Th37; hence ( a,b,c is_collinear & c <> a & c <> b ) by A6, A5, Th6, Th22, Th24; ::_thesis: verum end; theorem Th49: :: SEMI_AF1:49 for SAS being Semi_Affine_Space for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds b,c // b9,c9 proof let SAS be Semi_Affine_Space; ::_thesis: for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds b,c // b9,c9 let a, a9, b, b9, c, c9 be Element of SAS; ::_thesis: ( parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies b,c // b9,c9 ) assume that A1: parallelogram a,a9,b,b9 and A2: parallelogram a,a9,c,c9 ; ::_thesis: b,c // b9,c9 A3: ( a,a9 // c,c9 & a,c // a9,c9 ) by A2, Def3; not a,a9,c is_collinear by A2, Def3; then A4: not a,a9 // a,c by Def2; not a,a9,b is_collinear by A1, Def3; then A5: not a,a9 // a,b by Def2; ( a,a9 // b,b9 & a,b // a9,b9 ) by A1, Def3; hence b,c // b9,c9 by A5, A4, A3, Def1; ::_thesis: verum end; theorem Th50: :: SEMI_AF1:50 for SAS being Semi_Affine_Space for b, b9, c, a, a9, c9 being Element of SAS st not b,b9,c is_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds parallelogram b,b9,c,c9 proof let SAS be Semi_Affine_Space; ::_thesis: for b, b9, c, a, a9, c9 being Element of SAS st not b,b9,c is_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds parallelogram b,b9,c,c9 let b, b9, c, a, a9, c9 be Element of SAS; ::_thesis: ( not b,b9,c is_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9 ) assume that A1: not b,b9,c is_collinear and A2: parallelogram a,a9,b,b9 and A3: parallelogram a,a9,c,c9 ; ::_thesis: parallelogram b,b9,c,c9 A4: a,a9 // c,c9 by A3, Def3; ( a <> a9 & a,a9 // b,b9 ) by A2, Def3, Th36; then A5: b,b9 // c,c9 by A4, Def1; b,c // b9,c9 by A2, A3, Th49; hence parallelogram b,b9,c,c9 by A1, A5, Def3; ::_thesis: verum end; theorem Th51: :: SEMI_AF1:51 for SAS being Semi_Affine_Space for a, b, c, a9, b9, c9 being Element of SAS st a,b,c is_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds parallelogram b,b9,c,c9 proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, a9, b9, c9 being Element of SAS st a,b,c is_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds parallelogram b,b9,c,c9 let a, b, c, a9, b9, c9 be Element of SAS; ::_thesis: ( a,b,c is_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9 ) assume that A1: a,b,c is_collinear and A2: b <> c and A3: parallelogram a,a9,b,b9 and A4: parallelogram a,a9,c,c9 ; ::_thesis: parallelogram b,b9,c,c9 A5: b <> b9 by A3, Th36; a,b // a,c by A1, Def2; then A6: a,b // b,c by Th7; ( not a,a9,b is_collinear & a,a9 // b,b9 ) by A3, Def3; hence parallelogram b,b9,c,c9 by A2, A3, A4, A6, A5, Th23, Th50; ::_thesis: verum end; theorem Th52: :: SEMI_AF1:52 for SAS being Semi_Affine_Space for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 holds c,d // c9,d9 proof let SAS be Semi_Affine_Space; ::_thesis: for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 holds c,d // c9,d9 let a, a9, b, b9, c, c9, d, d9 be Element of SAS; ::_thesis: ( parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 implies c,d // c9,d9 ) assume that A1: parallelogram a,a9,b,b9 and A2: parallelogram a,a9,c,c9 and A3: parallelogram b,b9,d,d9 ; ::_thesis: c,d // c9,d9 A4: now__::_thesis:_(_not_a,a9,d_is_collinear_implies_c,d_//_c9,d9_) assume A5: not a,a9,d is_collinear ; ::_thesis: c,d // c9,d9 parallelogram b,b9,a,a9 by A1, Th43; then parallelogram a,a9,d,d9 by A3, A5, Th50; hence c,d // c9,d9 by A2, Th49; ::_thesis: verum end; A6: now__::_thesis:_(_b,b9,c_is_collinear_&_a,a9,d_is_collinear_implies_c,d_//_c9,d9_) A7: ( not a,a9,b is_collinear & a,a9 // a,a9 ) by A1, Th1, Th38; A8: a <> a9 by A1, Th36; assume that A9: b,b9,c is_collinear and A10: a,a9,d is_collinear ; ::_thesis: c,d // c9,d9 a <> b by A1, Th36; then consider x being Element of SAS such that A11: a,b,x is_collinear and A12: x <> a and A13: x <> b by Th48; a,b // a,x by A11, Def2; then consider y being Element of SAS such that A14: parallelogram a,a9,x,y by A12, A7, A8, Th23, Th44; A15: not x,y,d is_collinear by A10, A14, Th39; parallelogram b,b9,x,y by A1, A11, A13, A14, Th51; then A16: parallelogram x,y,d,d9 by A3, A15, Th50; not x,y,c is_collinear by A1, A9, A11, A13, A14, Th39, Th51; then parallelogram x,y,c,c9 by A2, A14, Th50; hence c,d // c9,d9 by A16, Th49; ::_thesis: verum end; now__::_thesis:_(_not_b,b9,c_is_collinear_implies_c,d_//_c9,d9_) assume not b,b9,c is_collinear ; ::_thesis: c,d // c9,d9 then parallelogram b,b9,c,c9 by A1, A2, Th50; hence c,d // c9,d9 by A3, Th49; ::_thesis: verum end; hence c,d // c9,d9 by A4, A6; ::_thesis: verum end; Lm1: for SAS being Semi_Affine_Space for a, b being Element of SAS st a <> b holds ex c, d being Element of SAS st parallelogram a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b being Element of SAS st a <> b holds ex c, d being Element of SAS st parallelogram a,b,c,d let a, b be Element of SAS; ::_thesis: ( a <> b implies ex c, d being Element of SAS st parallelogram a,b,c,d ) assume a <> b ; ::_thesis: ex c, d being Element of SAS st parallelogram a,b,c,d then consider c being Element of SAS such that A1: not a,b,c is_collinear by Th25; ex d being Element of SAS st parallelogram a,b,c,d by A1, Th44; hence ex c, d being Element of SAS st parallelogram a,b,c,d ; ::_thesis: verum end; theorem :: SEMI_AF1:53 for SAS being Semi_Affine_Space for a, d being Element of SAS st a <> d holds ex b, c being Element of SAS st parallelogram a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, d being Element of SAS st a <> d holds ex b, c being Element of SAS st parallelogram a,b,c,d let a, d be Element of SAS; ::_thesis: ( a <> d implies ex b, c being Element of SAS st parallelogram a,b,c,d ) assume a <> d ; ::_thesis: ex b, c being Element of SAS st parallelogram a,b,c,d then consider b being Element of SAS such that A1: not a,d,b is_collinear by Th25; not b,a,d is_collinear by A1, Th22; then consider c being Element of SAS such that A2: parallelogram b,a,d,c by Th44; parallelogram a,b,c,d by A2, Th43; hence ex b, c being Element of SAS st parallelogram a,b,c,d ; ::_thesis: verum end; definition let SAS be Semi_Affine_Space; let a, b, r, s be Element of SAS; pred congr a,b,r,s means :Def4: :: SEMI_AF1:def 4 ( ( a = b & r = s ) or ex p, q being Element of SAS st ( parallelogram p,q,a,b & parallelogram p,q,r,s ) ); end; :: deftheorem Def4 defines congr SEMI_AF1:def_4_:_ for SAS being Semi_Affine_Space for a, b, r, s being Element of SAS holds ( congr a,b,r,s iff ( ( a = b & r = s ) or ex p, q being Element of SAS st ( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) ); theorem Th54: :: SEMI_AF1:54 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st congr a,a,b,c holds b = c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st congr a,a,b,c holds b = c let a, b, c be Element of SAS; ::_thesis: ( congr a,a,b,c implies b = c ) assume congr a,a,b,c ; ::_thesis: b = c then ( ( a = a & b = c ) or ex p, q being Element of SAS st ( parallelogram p,q,a,a & parallelogram p,q,b,c ) ) by Def4; hence b = c by Th36; ::_thesis: verum end; theorem Th55: :: SEMI_AF1:55 for SAS being Semi_Affine_Space for a, b, c being Element of SAS st congr a,b,c,c holds a = b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS st congr a,b,c,c holds a = b let a, b, c be Element of SAS; ::_thesis: ( congr a,b,c,c implies a = b ) assume congr a,b,c,c ; ::_thesis: a = b then ( ( a = b & c = c ) or ex p, q being Element of SAS st ( parallelogram p,q,a,b & parallelogram p,q,c,c ) ) by Def4; hence a = b by Th36; ::_thesis: verum end; theorem Th56: :: SEMI_AF1:56 for SAS being Semi_Affine_Space for a, b being Element of SAS st congr a,b,b,a holds a = b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b being Element of SAS st congr a,b,b,a holds a = b let a, b be Element of SAS; ::_thesis: ( congr a,b,b,a implies a = b ) assume A1: congr a,b,b,a ; ::_thesis: a = b now__::_thesis:_not_a_<>_b assume a <> b ; ::_thesis: contradiction then ex p, q being Element of SAS st ( parallelogram p,q,a,b & parallelogram p,q,b,a ) by A1, Def4; hence contradiction by Th47; ::_thesis: verum end; hence a = b ; ::_thesis: verum end; theorem Th57: :: SEMI_AF1:57 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds a,b // c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds a,b // c,d let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies a,b // c,d ) assume A1: congr a,b,c,d ; ::_thesis: a,b // c,d now__::_thesis:_(_a_<>_b_implies_a,b_//_c,d_) assume a <> b ; ::_thesis: a,b // c,d then consider p, q being Element of SAS such that A2: parallelogram p,q,a,b and A3: parallelogram p,q,c,d by A1, Def4; A4: p,q // c,d by A3, Def3; ( p <> q & p,q // a,b ) by A2, Def3, Th36; hence a,b // c,d by A4, Def1; ::_thesis: verum end; hence a,b // c,d by Th3; ::_thesis: verum end; theorem Th58: :: SEMI_AF1:58 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds a,c // b,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds a,c // b,d let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies a,c // b,d ) assume A1: congr a,b,c,d ; ::_thesis: a,c // b,d A2: now__::_thesis:_(_a_<>_b_implies_a,c_//_b,d_) assume a <> b ; ::_thesis: a,c // b,d then ex p, q being Element of SAS st ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4; hence a,c // b,d by Th49; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_a,c_//_b,d_) assume A3: a = b ; ::_thesis: a,c // b,d then c = d by A1, Th54; hence a,c // b,d by A3, Th1; ::_thesis: verum end; hence a,c // b,d by A2; ::_thesis: verum end; theorem Th59: :: SEMI_AF1:59 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d & not a,b,c is_collinear holds parallelogram a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d & not a,b,c is_collinear holds parallelogram a,b,c,d let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d & not a,b,c is_collinear implies parallelogram a,b,c,d ) assume that A1: congr a,b,c,d and A2: not a,b,c is_collinear ; ::_thesis: parallelogram a,b,c,d ( a,b // c,d & a,c // b,d ) by A1, Th57, Th58; hence parallelogram a,b,c,d by A2, Def3; ::_thesis: verum end; theorem Th60: :: SEMI_AF1:60 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds congr a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds congr a,b,c,d let a, b, c, d be Element of SAS; ::_thesis: ( parallelogram a,b,c,d implies congr a,b,c,d ) A1: a,b // a,b by Th1; assume A2: parallelogram a,b,c,d ; ::_thesis: congr a,b,c,d then A3: ( not a,c,b is_collinear & a <> b ) by Th36, Th38; a <> c by A2, Th36; then consider p being Element of SAS such that A4: a,c,p is_collinear and A5: a <> p and A6: c <> p by Th48; a,c // a,p by A4, Def2; then consider q being Element of SAS such that A7: parallelogram a,p,b,q by A5, A1, A3, Th23, Th44; parallelogram a,b,p,q by A7, Th43; then parallelogram c,d,p,q by A2, A4, A6, Th51; then A8: parallelogram p,q,c,d by Th43; parallelogram p,q,a,b by A7, Th43; hence congr a,b,c,d by A8, Def4; ::_thesis: verum end; theorem Th61: :: SEMI_AF1:61 for SAS being Semi_Affine_Space for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b holds parallelogram r,s,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b holds parallelogram r,s,c,d let a, b, c, d, r, s be Element of SAS; ::_thesis: ( congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d ) assume that A1: congr a,b,c,d and A2: a,b,c is_collinear and A3: parallelogram r,s,a,b ; ::_thesis: parallelogram r,s,c,d now__::_thesis:_(_a_<>_b_implies_parallelogram_r,s,c,d_) A4: parallelogram a,b,r,s by A3, Th43; assume A5: a <> b ; ::_thesis: parallelogram r,s,c,d then consider p, q being Element of SAS such that A6: parallelogram p,q,a,b and A7: parallelogram p,q,c,d by A1, Def4; parallelogram a,b,p,q by A6, Th43; then A8: r,c // s,d by A7, A4, Th52; ( r,s // a,b & a,b // c,d ) by A1, A3, Def3, Th57; then A9: r,s // c,d by A5, Th8; not r,s,c is_collinear by A2, A3, Th39; hence parallelogram r,s,c,d by A9, A8, Def3; ::_thesis: verum end; hence parallelogram r,s,c,d by A3, Th36; ::_thesis: verum end; theorem Th62: :: SEMI_AF1:62 for SAS being Semi_Affine_Space for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds x = y proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds x = y let a, b, c, x, y be Element of SAS; ::_thesis: ( congr a,b,c,x & congr a,b,c,y implies x = y ) assume that A1: congr a,b,c,x and A2: congr a,b,c,y ; ::_thesis: x = y A3: now__::_thesis:_(_a_<>_b_&_not_a,b,c_is_collinear_implies_x_=_y_) assume that a <> b and A4: not a,b,c is_collinear ; ::_thesis: x = y ( parallelogram a,b,c,x & parallelogram a,b,c,y ) by A1, A2, A4, Th59; hence x = y by Th45; ::_thesis: verum end; A5: now__::_thesis:_(_a_<>_b_&_a,b,c_is_collinear_implies_x_=_y_) assume that A6: a <> b and A7: a,b,c is_collinear ; ::_thesis: x = y consider p, q being Element of SAS such that A8: parallelogram a,b,p,q by A6, Lm1; parallelogram p,q,a,b by A8, Th43; then ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A2, A7, Th61; hence x = y by Th45; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_x_=_y_) assume A9: a = b ; ::_thesis: x = y then c = x by A1, Th54; hence x = y by A2, A9, Th54; ::_thesis: verum end; hence x = y by A5, A3; ::_thesis: verum end; theorem Th63: :: SEMI_AF1:63 for SAS being Semi_Affine_Space for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d let a, b, c be Element of SAS; ::_thesis: ex d being Element of SAS st congr a,b,c,d A1: now__::_thesis:_(_a_=_b_implies_ex_d_being_Element_of_SAS_st_congr_a,b,c,d_) assume a = b ; ::_thesis: ex d being Element of SAS st congr a,b,c,d then congr a,b,c,c by Def4; hence ex d being Element of SAS st congr a,b,c,d ; ::_thesis: verum end; A2: now__::_thesis:_(_a_<>_b_&_a,b,c_is_collinear_implies_ex_d_being_Element_of_SAS_st_congr_a,b,c,d_) assume that A3: a <> b and A4: a,b,c is_collinear ; ::_thesis: ex d being Element of SAS st congr a,b,c,d consider p, q being Element of SAS such that A5: parallelogram a,b,p,q by A3, Lm1; not p,q,c is_collinear by A4, A5, Th39; then consider d being Element of SAS such that A6: parallelogram p,q,c,d by Th44; parallelogram p,q,a,b by A5, Th43; then congr a,b,c,d by A6, Def4; hence ex d being Element of SAS st congr a,b,c,d ; ::_thesis: verum end; now__::_thesis:_(_a_<>_b_&_not_a,b,c_is_collinear_implies_ex_d_being_Element_of_SAS_st_congr_a,b,c,d_) assume that a <> b and A7: not a,b,c is_collinear ; ::_thesis: ex d being Element of SAS st congr a,b,c,d ex d being Element of SAS st parallelogram a,b,c,d by A7, Th44; hence ex d being Element of SAS st congr a,b,c,d by Th60; ::_thesis: verum end; hence ex d being Element of SAS st congr a,b,c,d by A1, A2; ::_thesis: verum end; theorem Th64: :: SEMI_AF1:64 for SAS being Semi_Affine_Space for a, b being Element of SAS holds congr a,b,a,b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b being Element of SAS holds congr a,b,a,b let a, b be Element of SAS; ::_thesis: congr a,b,a,b now__::_thesis:_(_a_<>_b_implies_congr_a,b,a,b_) assume a <> b ; ::_thesis: congr a,b,a,b then consider p, q being Element of SAS such that A1: parallelogram a,b,p,q by Lm1; parallelogram p,q,a,b by A1, Th43; hence congr a,b,a,b by Def4; ::_thesis: verum end; hence congr a,b,a,b by Def4; ::_thesis: verum end; theorem Th65: :: SEMI_AF1:65 for SAS being Semi_Affine_Space for r, s, a, b, c, d being Element of SAS st congr r,s,a,b & congr r,s,c,d holds congr a,b,c,d proof let SAS be Semi_Affine_Space; ::_thesis: for r, s, a, b, c, d being Element of SAS st congr r,s,a,b & congr r,s,c,d holds congr a,b,c,d let r, s, a, b, c, d be Element of SAS; ::_thesis: ( congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d ) assume that A1: congr r,s,a,b and A2: congr r,s,c,d ; ::_thesis: congr a,b,c,d A3: now__::_thesis:_(_r_<>_s_&_not_r,s,a_is_collinear_&_not_r,s,c_is_collinear_implies_congr_a,b,c,d_) assume that r <> s and A4: ( not r,s,a is_collinear & not r,s,c is_collinear ) ; ::_thesis: congr a,b,c,d ( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, A2, A4, Th59; hence congr a,b,c,d by Def4; ::_thesis: verum end; A5: now__::_thesis:_(_r_<>_s_&_r,s,c_is_collinear_implies_congr_a,b,c,d_) assume that A6: r <> s and A7: r,s,c is_collinear ; ::_thesis: congr a,b,c,d consider p, q being Element of SAS such that A8: parallelogram p,q,r,s and A9: parallelogram p,q,a,b by A1, A6, Def4; parallelogram p,q,c,d by A2, A7, A8, Th61; hence congr a,b,c,d by A9, Def4; ::_thesis: verum end; A10: now__::_thesis:_(_r_<>_s_&_r,s,a_is_collinear_implies_congr_a,b,c,d_) assume that A11: r <> s and A12: r,s,a is_collinear ; ::_thesis: congr a,b,c,d consider p, q being Element of SAS such that A13: parallelogram p,q,r,s and A14: parallelogram p,q,c,d by A2, A11, Def4; parallelogram p,q,a,b by A1, A12, A13, Th61; hence congr a,b,c,d by A14, Def4; ::_thesis: verum end; now__::_thesis:_(_r_=_s_implies_congr_a,b,c,d_) assume r = s ; ::_thesis: congr a,b,c,d then ( a = b & c = d ) by A1, A2, Th54; hence congr a,b,c,d by Def4; ::_thesis: verum end; hence congr a,b,c,d by A10, A5, A3; ::_thesis: verum end; theorem Th66: :: SEMI_AF1:66 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds congr c,d,a,b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds congr c,d,a,b let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies congr c,d,a,b ) assume A1: congr a,b,c,d ; ::_thesis: congr c,d,a,b congr a,b,a,b by Th64; hence congr c,d,a,b by A1, Th65; ::_thesis: verum end; theorem Th67: :: SEMI_AF1:67 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds congr b,a,d,c proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds congr b,a,d,c let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies congr b,a,d,c ) assume A1: congr a,b,c,d ; ::_thesis: congr b,a,d,c A2: now__::_thesis:_(_a_<>_b_implies_congr_b,a,d,c_) assume a <> b ; ::_thesis: congr b,a,d,c then consider p, q being Element of SAS such that A3: ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4; ( parallelogram q,p,b,a & parallelogram q,p,d,c ) by A3, Th43; hence congr b,a,d,c by Def4; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_congr_b,a,d,c_) assume A4: a = b ; ::_thesis: congr b,a,d,c then c = d by A1, Th54; hence congr b,a,d,c by A4, Def4; ::_thesis: verum end; hence congr b,a,d,c by A2; ::_thesis: verum end; theorem Th68: :: SEMI_AF1:68 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds congr a,c,b,d proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds congr a,c,b,d let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies congr a,c,b,d ) assume A1: congr a,b,c,d ; ::_thesis: congr a,c,b,d A2: now__::_thesis:_(_a_=_c_implies_congr_a,c,b,d_) assume A3: a = c ; ::_thesis: congr a,c,b,d congr a,b,a,b by Th64; then b = d by A1, A3, Th62; hence congr a,c,b,d by A3, Def4; ::_thesis: verum end; A4: now__::_thesis:_(_a_<>_b_&_a_<>_c_&_a,b,c_is_collinear_implies_congr_a,c,b,d_) assume that A5: a <> b and A6: a <> c and A7: a,b,c is_collinear ; ::_thesis: congr a,c,b,d A8: a,b // a,c by A7, Def2; consider p, q being Element of SAS such that A9: parallelogram p,q,a,b and A10: parallelogram p,q,c,d by A1, A5, Def4; A11: a,p // a,p by Th1; ( not a,b,p is_collinear & a <> p ) by A9, Th36, Th38; then consider r being Element of SAS such that A12: parallelogram a,c,p,r by A6, A8, A11, Th23, Th44; A13: a,c // p,r by A12, Def3; A14: p,q // c,d by A10, Def3; ( p <> q & p,q // a,b ) by A9, Def3, Th36; then A15: a,b // c,d by A14, Def1; then a,c // b,d by A5, A7, Th32; then A16: p,r // b,d by A6, A13, Def1; parallelogram p,r,a,c by A12, Th43; then A17: p,a // r,c by Def3; ( p,a // q,b & p <> a ) by A9, Def3, Th36; then A18: r,c // q,b by A17, Def1; p,c // q,d by A10, Def3; then A19: q,d // p,c by Th6; p,q // a,b by A9, Def3; then A20: a,b // p,q by Th6; A21: a,c // p,r by A12, Def3; a,b // a,c by A7, Def2; then a,c // p,q by A5, A20, Def1; then p,q // p,r by A6, A21, Def1; then A22: r,q // r,p by Th7; a,c,b is_collinear by A7, Th22; then A23: not p,r,b is_collinear by A12, Th39; A24: parallelogram p,r,a,c by A12, Th43; c,b // c,d by A5, A7, A15, Th33; then b,c // b,d by Th7; then p,b // r,d by A22, A18, A19, Def1; then parallelogram p,r,b,d by A23, A16, Def3; hence congr a,c,b,d by A24, Def4; ::_thesis: verum end; A25: now__::_thesis:_(_a_<>_b_&_a_<>_c_&_not_a,b,c_is_collinear_implies_congr_a,c,b,d_) assume that a <> b and a <> c and A26: not a,b,c is_collinear ; ::_thesis: congr a,c,b,d parallelogram a,b,c,d by A1, A26, Th59; then parallelogram a,c,b,d by Th43; hence congr a,c,b,d by Th60; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_congr_a,c,b,d_) assume A27: a = b ; ::_thesis: congr a,c,b,d then c = d by A1, Th54; hence congr a,c,b,d by A27, Th64; ::_thesis: verum end; hence congr a,c,b,d by A2, A4, A25; ::_thesis: verum end; theorem Th69: :: SEMI_AF1:69 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st congr a,b,c,d holds ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) let a, b, c, d be Element of SAS; ::_thesis: ( congr a,b,c,d implies ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) ) assume A1: congr a,b,c,d ; ::_thesis: ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) then congr c,d,a,b by Th66; then A2: congr d,c,b,a by Th67; ( congr b,a,d,c & congr a,c,b,d ) by A1, Th67, Th68; hence ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) by A2, Th67, Th68; ::_thesis: verum end; theorem Th70: :: SEMI_AF1:70 for SAS being Semi_Affine_Space for a, b, p, q, c, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds congr a,c,p,s proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, p, q, c, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds congr a,c,p,s let a, b, p, q, c, s be Element of SAS; ::_thesis: ( congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s ) assume ( congr a,b,p,q & congr b,c,q,s ) ; ::_thesis: congr a,c,p,s then ( congr b,q,a,p & congr b,q,c,s ) by Th69; then congr a,p,c,s by Th65; hence congr a,c,p,s by Th68; ::_thesis: verum end; theorem Th71: :: SEMI_AF1:71 for SAS being Semi_Affine_Space for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds congr b,c,r,q proof let SAS be Semi_Affine_Space; ::_thesis: for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds congr b,c,r,q let b, a, p, q, c, r be Element of SAS; ::_thesis: ( congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q ) assume that A1: congr b,a,p,q and A2: congr c,a,p,r ; ::_thesis: congr b,c,r,q A3: congr r,p,a,c by A2, Th69; consider s being Element of SAS such that A4: congr p,q,r,s by Th63; congr r,p,s,q by A4, Th69; then A5: congr a,c,s,q by A3, Th65; congr p,q,b,a by A1, Th69; then congr b,a,r,s by A4, Th65; hence congr b,c,r,q by A5, Th70; ::_thesis: verum end; theorem :: SEMI_AF1:72 for SAS being Semi_Affine_Space for a, o, p, b, q being Element of SAS st congr a,o,o,p & congr b,o,o,q holds congr a,b,q,p by Th71; theorem Th73: :: SEMI_AF1:73 for SAS being Semi_Affine_Space for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds b,c // q,r proof let SAS be Semi_Affine_Space; ::_thesis: for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds b,c // q,r let b, a, p, q, c, r be Element of SAS; ::_thesis: ( congr b,a,p,q & congr c,a,p,r implies b,c // q,r ) assume ( congr b,a,p,q & congr c,a,p,r ) ; ::_thesis: b,c // q,r then b,c // r,q by Th57, Th71; hence b,c // q,r by Th6; ::_thesis: verum end; theorem :: SEMI_AF1:74 for SAS being Semi_Affine_Space for a, o, p, b, q being Element of SAS st congr a,o,o,p & congr b,o,o,q holds a,b // p,q by Th73; definition let SAS be Semi_Affine_Space; let a, b, o be Element of SAS; func sum (a,b,o) -> Element of SAS means :Def5: :: SEMI_AF1:def 5 congr o,a,b,it; correctness existence ex b1 being Element of SAS st congr o,a,b,b1; uniqueness for b1, b2 being Element of SAS st congr o,a,b,b1 & congr o,a,b,b2 holds b1 = b2; by Th62, Th63; end; :: deftheorem Def5 defines sum SEMI_AF1:def_5_:_ for SAS being Semi_Affine_Space for a, b, o, b5 being Element of SAS holds ( b5 = sum (a,b,o) iff congr o,a,b,b5 ); definition let SAS be Semi_Affine_Space; let a, o be Element of SAS; func opposite (a,o) -> Element of SAS means :Def6: :: SEMI_AF1:def 6 sum (a,it,o) = o; existence ex b1 being Element of SAS st sum (a,b1,o) = o proof consider b being Element of SAS such that A1: congr a,o,o,b by Th63; take b ; ::_thesis: sum (a,b,o) = o congr o,a,b,o by A1, Th67; hence sum (a,b,o) = o by Def5; ::_thesis: verum end; uniqueness for b1, b2 being Element of SAS st sum (a,b1,o) = o & sum (a,b2,o) = o holds b1 = b2 proof let b1, b2 be Element of SAS; ::_thesis: ( sum (a,b1,o) = o & sum (a,b2,o) = o implies b1 = b2 ) assume that A2: sum (a,b1,o) = o and A3: sum (a,b2,o) = o ; ::_thesis: b1 = b2 congr o,a,b2,o by A3, Def5; then A4: congr a,o,o,b2 by Th67; congr o,a,b1,o by A2, Def5; then congr a,o,o,b1 by Th67; hence b1 = b2 by A4, Th62; ::_thesis: verum end; end; :: deftheorem Def6 defines opposite SEMI_AF1:def_6_:_ for SAS being Semi_Affine_Space for a, o, b4 being Element of SAS holds ( b4 = opposite (a,o) iff sum (a,b4,o) = o ); definition let SAS be Semi_Affine_Space; let a, b, o be Element of SAS; func diff (a,b,o) -> Element of SAS equals :: SEMI_AF1:def 7 sum (a,(opposite (b,o)),o); correctness coherence sum (a,(opposite (b,o)),o) is Element of SAS; ; end; :: deftheorem defines diff SEMI_AF1:def_7_:_ for SAS being Semi_Affine_Space for a, b, o being Element of SAS holds diff (a,b,o) = sum (a,(opposite (b,o)),o); theorem Th75: :: SEMI_AF1:75 for SAS being Semi_Affine_Space for a, o being Element of SAS holds sum (a,o,o) = a proof let SAS be Semi_Affine_Space; ::_thesis: for a, o being Element of SAS holds sum (a,o,o) = a let a, o be Element of SAS; ::_thesis: sum (a,o,o) = a congr o,a,o,a by Th64; hence sum (a,o,o) = a by Def5; ::_thesis: verum end; theorem :: SEMI_AF1:76 for SAS being Semi_Affine_Space for a, o being Element of SAS ex x being Element of SAS st sum (a,x,o) = o proof let SAS be Semi_Affine_Space; ::_thesis: for a, o being Element of SAS ex x being Element of SAS st sum (a,x,o) = o let a, o be Element of SAS; ::_thesis: ex x being Element of SAS st sum (a,x,o) = o consider x being Element of SAS such that A1: congr a,o,o,x by Th63; A2: congr o,a,x, sum (a,x,o) by Def5; congr o,a,x,o by A1, Th69; hence ex x being Element of SAS st sum (a,x,o) = o by A2, Th62; ::_thesis: verum end; theorem :: SEMI_AF1:77 for SAS being Semi_Affine_Space for a, b, o, c being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, o, c being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o) let a, b, o, c be Element of SAS; ::_thesis: sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o) ( congr o,a,b, sum (a,b,o) & congr o,a, sum (b,c,o), sum (a,(sum (b,c,o)),o) ) by Def5; then A1: congr b, sum (a,b,o), sum (b,c,o), sum (a,(sum (b,c,o)),o) by Th65; congr o,b,c, sum (b,c,o) by Def5; then A2: congr b,o, sum (b,c,o),c by Th69; congr o, sum (a,b,o),c, sum ((sum (a,b,o)),c,o) by Def5; then congr b, sum (a,b,o), sum (b,c,o), sum ((sum (a,b,o)),c,o) by A2, Th70; hence sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o) by A1, Th62; ::_thesis: verum end; theorem Th78: :: SEMI_AF1:78 for SAS being Semi_Affine_Space for a, b, o being Element of SAS holds sum (a,b,o) = sum (b,a,o) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, o being Element of SAS holds sum (a,b,o) = sum (b,a,o) let a, b, o be Element of SAS; ::_thesis: sum (a,b,o) = sum (b,a,o) congr o,b,a, sum (b,a,o) by Def5; then congr o,a,b, sum (b,a,o) by Th69; hence sum (a,b,o) = sum (b,a,o) by Def5; ::_thesis: verum end; theorem :: SEMI_AF1:79 for SAS being Semi_Affine_Space for a, o being Element of SAS st sum (a,a,o) = o holds a = o proof let SAS be Semi_Affine_Space; ::_thesis: for a, o being Element of SAS st sum (a,a,o) = o holds a = o let a, o be Element of SAS; ::_thesis: ( sum (a,a,o) = o implies a = o ) assume sum (a,a,o) = o ; ::_thesis: a = o then congr o,a,a,o by Def5; hence a = o by Th56; ::_thesis: verum end; theorem :: SEMI_AF1:80 for SAS being Semi_Affine_Space for a, x, o, y being Element of SAS st sum (a,x,o) = sum (a,y,o) holds x = y proof let SAS be Semi_Affine_Space; ::_thesis: for a, x, o, y being Element of SAS st sum (a,x,o) = sum (a,y,o) holds x = y let a, x, o, y be Element of SAS; ::_thesis: ( sum (a,x,o) = sum (a,y,o) implies x = y ) assume A1: sum (a,x,o) = sum (a,y,o) ; ::_thesis: x = y congr o,a,x, sum (a,x,o) by Def5; then A2: congr a,o, sum (a,x,o),x by Th69; congr o,a,y, sum (a,y,o) by Def5; then congr a,o, sum (a,x,o),y by A1, Th69; hence x = y by A2, Th62; ::_thesis: verum end; theorem Th81: :: SEMI_AF1:81 for SAS being Semi_Affine_Space for a, o being Element of SAS holds congr a,o,o, opposite (a,o) proof let SAS be Semi_Affine_Space; ::_thesis: for a, o being Element of SAS holds congr a,o,o, opposite (a,o) let a, o be Element of SAS; ::_thesis: congr a,o,o, opposite (a,o) ( sum (a,(opposite (a,o)),o) = o & congr o,a, opposite (a,o), sum (a,(opposite (a,o)),o) ) by Def5, Def6; hence congr a,o,o, opposite (a,o) by Th69; ::_thesis: verum end; theorem Th82: :: SEMI_AF1:82 for SAS being Semi_Affine_Space for a, o, b being Element of SAS st opposite (a,o) = opposite (b,o) holds a = b proof let SAS be Semi_Affine_Space; ::_thesis: for a, o, b being Element of SAS st opposite (a,o) = opposite (b,o) holds a = b let a, o, b be Element of SAS; ::_thesis: ( opposite (a,o) = opposite (b,o) implies a = b ) assume A1: opposite (a,o) = opposite (b,o) ; ::_thesis: a = b congr a,o,o, opposite (a,o) by Th81; then A2: congr opposite (a,o),o,o,a by Th69; congr b,o,o, opposite (b,o) by Th81; then congr opposite (a,o),o,o,b by A1, Th69; hence a = b by A2, Th62; ::_thesis: verum end; theorem :: SEMI_AF1:83 for SAS being Semi_Affine_Space for a, b, o being Element of SAS holds a,b // opposite (a,o), opposite (b,o) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, o being Element of SAS holds a,b // opposite (a,o), opposite (b,o) let a, b, o be Element of SAS; ::_thesis: a,b // opposite (a,o), opposite (b,o) sum (b,(opposite (b,o)),o) = o by Def6; then congr o,b, opposite (b,o),o by Def5; then A1: congr b,o,o, opposite (b,o) by Th69; sum (a,(opposite (a,o)),o) = o by Def6; then congr o,a, opposite (a,o),o by Def5; then congr a,o,o, opposite (a,o) by Th69; hence a,b // opposite (a,o), opposite (b,o) by A1, Th73; ::_thesis: verum end; theorem :: SEMI_AF1:84 for SAS being Semi_Affine_Space for o being Element of SAS holds opposite (o,o) = o proof let SAS be Semi_Affine_Space; ::_thesis: for o being Element of SAS holds opposite (o,o) = o let o be Element of SAS; ::_thesis: opposite (o,o) = o sum (o,(opposite (o,o)),o) = o by Def6; then sum ((opposite (o,o)),o,o) = o by Th78; hence opposite (o,o) = o by Th75; ::_thesis: verum end; theorem Th85: :: SEMI_AF1:85 for SAS being Semi_Affine_Space for p, q, r, o being Element of SAS holds p,q // sum (p,r,o), sum (q,r,o) proof let SAS be Semi_Affine_Space; ::_thesis: for p, q, r, o being Element of SAS holds p,q // sum (p,r,o), sum (q,r,o) let p, q, r, o be Element of SAS; ::_thesis: p,q // sum (p,r,o), sum (q,r,o) congr o,p,r, sum (p,r,o) by Def5; then A1: congr p,o, sum (p,r,o),r by Th69; congr o,q,r, sum (q,r,o) by Def5; hence p,q // sum (p,r,o), sum (q,r,o) by A1, Th57, Th70; ::_thesis: verum end; theorem :: SEMI_AF1:86 for SAS being Semi_Affine_Space for p, q, r, s, o being Element of SAS st p,q // r,s holds p,q // sum (p,r,o), sum (q,s,o) proof let SAS be Semi_Affine_Space; ::_thesis: for p, q, r, s, o being Element of SAS st p,q // r,s holds p,q // sum (p,r,o), sum (q,s,o) let p, q, r, s, o be Element of SAS; ::_thesis: ( p,q // r,s implies p,q // sum (p,r,o), sum (q,s,o) ) assume A1: p,q // r,s ; ::_thesis: p,q // sum (p,r,o), sum (q,s,o) now__::_thesis:_(_p_<>_q_&_r_<>_s_implies_p,q_//_sum_(p,r,o),_sum_(q,s,o)_) consider t being Element of SAS such that A2: congr o,q,r,t by Th63; assume that A3: p <> q and A4: r <> s ; ::_thesis: p,q // sum (p,r,o), sum (q,s,o) congr o,q,s, sum (q,s,o) by Def5; then congr r,t,s, sum (q,s,o) by A2, Th65; then A5: congr r,s,t, sum (q,s,o) by Th69; then A6: t <> sum (q,s,o) by A4, Th55; r,s // t, sum (q,s,o) by A5, Th57; then A7: p,q // t, sum (q,s,o) by A1, A4, Th8; congr o,p,r, sum (p,r,o) by Def5; then congr p,o, sum (p,r,o),r by Th69; then p,q // sum (p,r,o),t by A2, Th57, Th70; then p,q // t, sum (p,r,o) by Th6; then t, sum (q,s,o) // t, sum (p,r,o) by A3, A7, Def1; then t, sum (q,s,o) // sum (p,r,o), sum (q,s,o) by Th7; hence p,q // sum (p,r,o), sum (q,s,o) by A6, A7, Th8; ::_thesis: verum end; hence p,q // sum (p,r,o), sum (q,s,o) by Th3, Th85; ::_thesis: verum end; theorem Th87: :: SEMI_AF1:87 for SAS being Semi_Affine_Space for a, b, o being Element of SAS holds ( diff (a,b,o) = o iff a = b ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, o being Element of SAS holds ( diff (a,b,o) = o iff a = b ) let a, b, o be Element of SAS; ::_thesis: ( diff (a,b,o) = o iff a = b ) ( diff (a,b,o) = o implies a = b ) proof assume diff (a,b,o) = o ; ::_thesis: a = b then opposite (a,o) = opposite (b,o) by Def6; hence a = b by Th82; ::_thesis: verum end; hence ( diff (a,b,o) = o iff a = b ) by Def6; ::_thesis: verum end; theorem Th88: :: SEMI_AF1:88 for SAS being Semi_Affine_Space for o, b, a being Element of SAS holds o, diff (b,a,o) // a,b proof let SAS be Semi_Affine_Space; ::_thesis: for o, b, a being Element of SAS holds o, diff (b,a,o) // a,b let o, b, a be Element of SAS; ::_thesis: o, diff (b,a,o) // a,b congr a,o,o, opposite (a,o) by Th81; then A1: congr o, opposite (a,o),a,o by Th69; congr o,b, opposite (a,o), sum (b,(opposite (a,o)),o) by Def5; then congr o, opposite (a,o),b, diff (b,a,o) by Th69; then congr a,o,b, diff (b,a,o) by A1, Th65; then congr o, diff (b,a,o),a,b by Th69; hence o, diff (b,a,o) // a,b by Th57; ::_thesis: verum end; theorem :: SEMI_AF1:89 for SAS being Semi_Affine_Space for o, b, a, d, c being Element of SAS holds ( o, diff (b,a,o), diff (d,c,o) is_collinear iff a,b // c,d ) proof let SAS be Semi_Affine_Space; ::_thesis: for o, b, a, d, c being Element of SAS holds ( o, diff (b,a,o), diff (d,c,o) is_collinear iff a,b // c,d ) let o, b, a, d, c be Element of SAS; ::_thesis: ( o, diff (b,a,o), diff (d,c,o) is_collinear iff a,b // c,d ) A1: ( a,b // c,d implies o, diff (b,a,o), diff (d,c,o) is_collinear ) proof assume A2: a,b // c,d ; ::_thesis: o, diff (b,a,o), diff (d,c,o) is_collinear A3: now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_o,_diff_(b,a,o),_diff_(d,c,o)_is_collinear_) o, diff (d,c,o) // c,d by Th88; then A4: c,d // o, diff (d,c,o) by Th6; assume that A5: a <> b and A6: c <> d ; ::_thesis: o, diff (b,a,o), diff (d,c,o) is_collinear o, diff (b,a,o) // a,b by Th88; then a,b // o, diff (b,a,o) by Th6; then o, diff (b,a,o) // c,d by A2, A5, Def1; then o, diff (b,a,o) // o, diff (d,c,o) by A6, A4, Th8; hence o, diff (b,a,o), diff (d,c,o) is_collinear by Def2; ::_thesis: verum end; now__::_thesis:_(_(_a_=_b_or_c_=_d_)_implies_o,_diff_(b,a,o),_diff_(d,c,o)_is_collinear_) assume ( a = b or c = d ) ; ::_thesis: o, diff (b,a,o), diff (d,c,o) is_collinear then ( o = diff (b,a,o) or o = diff (d,c,o) ) by Th87; then o, diff (b,a,o) // o, diff (d,c,o) by Def1, Th3; hence o, diff (b,a,o), diff (d,c,o) is_collinear by Def2; ::_thesis: verum end; hence o, diff (b,a,o), diff (d,c,o) is_collinear by A3; ::_thesis: verum end; ( o, diff (b,a,o), diff (d,c,o) is_collinear implies a,b // c,d ) proof assume A7: o, diff (b,a,o), diff (d,c,o) is_collinear ; ::_thesis: a,b // c,d A8: now__::_thesis:_(_o_<>_diff_(b,a,o)_&_o_<>_diff_(d,c,o)_implies_a,b_//_c,d_) A9: o, diff (d,c,o) // c,d by Th88; assume that A10: o <> diff (b,a,o) and A11: o <> diff (d,c,o) ; ::_thesis: a,b // c,d ( o, diff (b,a,o) // o, diff (d,c,o) & o, diff (b,a,o) // a,b ) by A7, Def2, Th88; then o, diff (d,c,o) // a,b by A10, Def1; hence a,b // c,d by A11, A9, Def1; ::_thesis: verum end; now__::_thesis:_(_(_o_=_diff_(b,a,o)_or_o_=_diff_(d,c,o)_)_implies_a,b_//_c,d_) assume ( o = diff (b,a,o) or o = diff (d,c,o) ) ; ::_thesis: a,b // c,d then ( a = b or c = d ) by Th87; hence a,b // c,d by Def1, Th3; ::_thesis: verum end; hence a,b // c,d by A8; ::_thesis: verum end; hence ( o, diff (b,a,o), diff (d,c,o) is_collinear iff a,b // c,d ) by A1; ::_thesis: verum end; definition let SAS be Semi_Affine_Space; let a, b, c, d, o be Element of SAS; pred trap a,b,c,d,o means :Def8: :: SEMI_AF1:def 8 ( not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear & a,c // b,d ); end; :: deftheorem Def8 defines trap SEMI_AF1:def_8_:_ for SAS being Semi_Affine_Space for a, b, c, d, o being Element of SAS holds ( trap a,b,c,d,o iff ( not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear & a,c // b,d ) ); definition let SAS be Semi_Affine_Space; let o, p be Element of SAS; pred qtrap o,p means :Def9: :: SEMI_AF1:def 9 for b, c being Element of SAS ex d being Element of SAS st ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ); end; :: deftheorem Def9 defines qtrap SEMI_AF1:def_9_:_ for SAS being Semi_Affine_Space for o, p being Element of SAS holds ( qtrap o,p iff for b, c being Element of SAS ex d being Element of SAS st ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) ); theorem Th90: :: SEMI_AF1:90 for SAS being Semi_Affine_Space for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds ( o <> a & a <> c & c <> o ) proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds ( o <> a & a <> c & c <> o ) let a, b, c, d, o be Element of SAS; ::_thesis: ( trap a,b,c,d,o implies ( o <> a & a <> c & c <> o ) ) assume trap a,b,c,d,o ; ::_thesis: ( o <> a & a <> c & c <> o ) then not o,a,c is_collinear by Def8; hence ( o <> a & a <> c & c <> o ) by Th24; ::_thesis: verum end; theorem :: SEMI_AF1:91 for SAS being Semi_Affine_Space for a, b, c, x, o, y being Element of SAS st trap a,b,c,x,o & trap a,b,c,y,o holds x = y proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, x, o, y being Element of SAS st trap a,b,c,x,o & trap a,b,c,y,o holds x = y let a, b, c, x, o, y be Element of SAS; ::_thesis: ( trap a,b,c,x,o & trap a,b,c,y,o implies x = y ) assume that A1: trap a,b,c,x,o and A2: trap a,b,c,y,o ; ::_thesis: x = y A3: ( a,c // b,x & a,c // b,y ) by A1, A2, Def8; A4: ( not o,a,c is_collinear & o,a,b is_collinear ) by A1, Def8; ( o,c,x is_collinear & o,c,y is_collinear ) by A1, A2, Def8; hence x = y by A4, A3, Th34; ::_thesis: verum end; theorem :: SEMI_AF1:92 for SAS being Semi_Affine_Space for o, a, b being Element of SAS st not o,a,b is_collinear holds trap a,o,b,o,o proof let SAS be Semi_Affine_Space; ::_thesis: for o, a, b being Element of SAS st not o,a,b is_collinear holds trap a,o,b,o,o let o, a, b be Element of SAS; ::_thesis: ( not o,a,b is_collinear implies trap a,o,b,o,o ) assume A1: not o,a,b is_collinear ; ::_thesis: trap a,o,b,o,o A2: a,b // o,o by Def1; ( o,a,o is_collinear & o,b,o is_collinear ) by Th24; hence trap a,o,b,o,o by A1, A2, Def8; ::_thesis: verum end; theorem Th93: :: SEMI_AF1:93 for SAS being Semi_Affine_Space for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds trap c,d,a,b,o proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds trap c,d,a,b,o let a, b, c, d, o be Element of SAS; ::_thesis: ( trap a,b,c,d,o implies trap c,d,a,b,o ) assume A1: trap a,b,c,d,o ; ::_thesis: trap c,d,a,b,o then not o,a,c is_collinear by Def8; then A2: not o,c,a is_collinear by Th22; a,c // b,d by A1, Def8; then A3: c,a // d,b by Th6; ( o,a,b is_collinear & o,c,d is_collinear ) by A1, Def8; hence trap c,d,a,b,o by A2, A3, Def8; ::_thesis: verum end; theorem Th94: :: SEMI_AF1:94 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st trap a,b,c,d,d holds d = b proof let SAS be Semi_Affine_Space; ::_thesis: for a, b, c, d being Element of SAS st trap a,b,c,d,d holds d = b let a, b, c, d be Element of SAS; ::_thesis: ( trap a,b,c,d,d implies d = b ) assume A1: trap a,b,c,d,d ; ::_thesis: d = b then a,c // b,d by Def8; then A2: d,b // a,c by Th6; d,a,b is_collinear by A1, Def8; then d,a // d,b by Def2; then A3: d,b // a,d by Th6; assume not d = b ; ::_thesis: contradiction then a,d // a,c by A3, A2, Def1; then A4: d,a // d,c by Th7; not d,a,c is_collinear by A1, Def8; hence contradiction by A4, Def2; ::_thesis: verum end; theorem Th95: :: SEMI_AF1:95 for SAS being Semi_Affine_Space for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds not o,b,d is_collinear proof let SAS be Semi_Affine_Space; ::_thesis: for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds not o,b,d is_collinear let o, b, a, c, d be Element of SAS; ::_thesis: ( o <> b & trap a,b,c,d,o implies not o,b,d is_collinear ) assume that A1: o <> b and A2: trap a,b,c,d,o ; ::_thesis: not o,b,d is_collinear o,a,b is_collinear by A2, Def8; then A3: o,a // o,b by Def2; o,c,d is_collinear by A2, Def8; then A4: o,c // o,d by Def2; ( o <> d & not o,a,c is_collinear ) by A1, A2, Def8, Th94; hence not o,b,d is_collinear by A1, A3, A4, Th23; ::_thesis: verum end; theorem :: SEMI_AF1:96 for SAS being Semi_Affine_Space for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds trap b,a,d,c,o proof let SAS be Semi_Affine_Space; ::_thesis: for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds trap b,a,d,c,o let o, b, a, c, d be Element of SAS; ::_thesis: ( o <> b & trap a,b,c,d,o implies trap b,a,d,c,o ) assume that A1: o <> b and A2: trap a,b,c,d,o ; ::_thesis: trap b,a,d,c,o o,a,b is_collinear by A2, Def8; then A3: o,b,a is_collinear by Th22; a,c // b,d by A2, Def8; then A4: b,d // a,c by Th6; o,c,d is_collinear by A2, Def8; then A5: o,d,c is_collinear by Th22; not o,b,d is_collinear by A1, A2, Th95; hence trap b,a,d,c,o by A3, A5, A4, Def8; ::_thesis: verum end; theorem :: SEMI_AF1:97 for SAS being Semi_Affine_Space for a, b, c, d being Element of SAS st trap a,b,c,d,b holds b = d by Th93, Th94; theorem Th98: :: SEMI_AF1:98 for SAS being Semi_Affine_Space for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o holds b,c // q,r proof let SAS be Semi_Affine_Space; ::_thesis: for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o holds b,c // q,r let a, p, b, q, o, c, r be Element of SAS; ::_thesis: ( trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r ) assume that A1: trap a,p,b,q,o and A2: trap a,p,c,r,o ; ::_thesis: b,c // q,r not o,a,b is_collinear by A1, Def8; then A3: not o,a // o,b by Def2; o,c,r is_collinear by A2, Def8; then A4: o,c // o,r by Def2; not o,a,c is_collinear by A2, Def8; then A5: not o,a // o,c by Def2; o,b,q is_collinear by A1, Def8; then A6: o,b // o,q by Def2; o,a,p is_collinear by A1, Def8; then A7: o,a // o,p by Def2; ( a,b // p,q & a,c // p,r ) by A1, A2, Def8; hence b,c // q,r by A3, A7, A6, A5, A4, Def1; ::_thesis: verum end; theorem Th99: :: SEMI_AF1:99 for SAS being Semi_Affine_Space for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear holds trap b,q,c,r,o proof let SAS be Semi_Affine_Space; ::_thesis: for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear holds trap b,q,c,r,o let a, p, b, q, o, c, r be Element of SAS; ::_thesis: ( trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear implies trap b,q,c,r,o ) assume that A1: ( trap a,p,b,q,o & trap a,p,c,r,o ) and A2: not o,b,c is_collinear ; ::_thesis: trap b,q,c,r,o A3: b,c // q,r by A1, Th98; ( o,b,q is_collinear & o,c,r is_collinear ) by A1, Def8; hence trap b,q,c,r,o by A2, A3, Def8; ::_thesis: verum end; theorem :: SEMI_AF1:100 for SAS being Semi_Affine_Space for a, p, b, q, o, c, r, d, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds c,d // r,s proof let SAS be Semi_Affine_Space; ::_thesis: for a, p, b, q, o, c, r, d, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds c,d // r,s let a, p, b, q, o, c, r, d, s be Element of SAS; ::_thesis: ( trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s ) assume that A1: trap a,p,b,q,o and A2: trap a,p,c,r,o and A3: trap b,q,d,s,o ; ::_thesis: c,d // r,s A4: now__::_thesis:_(_not_o,a,d_is_collinear_implies_c,d_//_r,s_) assume A5: not o,a,d is_collinear ; ::_thesis: c,d // r,s trap b,q,a,p,o by A1, Th93; then trap a,p,d,s,o by A3, A5, Th99; hence c,d // r,s by A2, Th98; ::_thesis: verum end; A6: now__::_thesis:_(_o_<>_p_&_o,b,c_is_collinear_&_o,a,d_is_collinear_implies_c,d_//_r,s_) not o,a,b is_collinear by A1, Def8; then not b,a,o is_collinear by Th22; then consider x being Element of SAS such that A7: parallelogram b,a,o,x by Th44; o,b,q is_collinear by A1, Def8; then o,b // o,q by Def2; then A8: b,o // q,o by Th6; A9: o,x // o,x by Th1; ( b,o // a,x & b <> o ) by A7, Def3, Th36; then A10: q,o // a,x by A8, Def1; A11: not o,x,b is_collinear by A7, Th38; A12: o <> d by A3, Th90; assume that A13: o <> p and A14: o,b,c is_collinear and A15: o,a,d is_collinear ; ::_thesis: c,d // r,s not o,p,q is_collinear by A1, A13, Th95; then not q,p,o is_collinear by Th22; then consider y being Element of SAS such that A16: parallelogram q,p,o,y by Th44; A17: not o,x,a is_collinear by A7, Th38; A18: o <> c by A2, Th90; a,b // p,q by A1, Def8; then A19: b,a // q,p by Th6; A20: o,a,p is_collinear by A1, Def8; ( b,a // o,x & b <> a ) by A7, Def3, Th36; then A21: q,p // o,x by A19, Def1; A22: o <> x by A7, Th36; ( q <> p & q,p // o,y ) by A16, Def3, Th36; then o,x // o,y by A21, Def1; then A23: o,x,y is_collinear by Def2; ( q,o // p,y & q <> o ) by A16, Def3, Th36; then A24: a,x // p,y by A10, Def1; not o,a,x is_collinear by A7, Th38; then A25: trap a,p,x,y,o by A23, A24, A20, Def8; not o,b,x is_collinear by A7, Th38; then A26: trap b,q,x,y,o by A1, A25, Th99; o,a // o,d by A15, Def2; then A27: trap x,y,d,s,o by A3, A26, A22, A12, A17, A9, Th23, Th99; o,b // o,c by A14, Def2; then trap x,y,c,r,o by A2, A25, A11, A22, A18, A9, Th23, Th99; hence c,d // r,s by A27, Th98; ::_thesis: verum end; A28: now__::_thesis:_(_o_=_p_implies_c,d_//_r,s_) assume A29: o = p ; ::_thesis: c,d // r,s then o = q by A1, Th93, Th94; then A30: o = s by A3, Th93, Th94; o = r by A2, A29, Th93, Th94; hence c,d // r,s by A30, Def1; ::_thesis: verum end; now__::_thesis:_(_not_o,b,c_is_collinear_implies_c,d_//_r,s_) assume not o,b,c is_collinear ; ::_thesis: c,d // r,s then trap b,q,c,r,o by A1, A2, Th99; hence c,d // r,s by A3, Th98; ::_thesis: verum end; hence c,d // r,s by A4, A28, A6; ::_thesis: verum end; theorem Th101: :: SEMI_AF1:101 for SAS being Semi_Affine_Space for o, a being Element of SAS ex p being Element of SAS st ( o,a,p is_collinear & qtrap o,p ) proof let SAS be Semi_Affine_Space; ::_thesis: for o, a being Element of SAS ex p being Element of SAS st ( o,a,p is_collinear & qtrap o,p ) let o, a be Element of SAS; ::_thesis: ex p being Element of SAS st ( o,a,p is_collinear & qtrap o,p ) consider p being Element of SAS such that A1: for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) by Def1; take p ; ::_thesis: ( o,a,p is_collinear & qtrap o,p ) now__::_thesis:_(_o,a,p_is_collinear_&_(_for_b,_c_being_Element_of_SAS_ex_d_being_Element_of_SAS_st_ (_o,p,b_is_collinear_implies_(_o,c,d_is_collinear_&_p,c_//_b,d_)_)_)_) thus o,a,p is_collinear by A1, Def2; ::_thesis: for b, c being Element of SAS ex d being Element of SAS st ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) let b, c be Element of SAS; ::_thesis: ex d being Element of SAS st ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) consider d being Element of SAS such that A2: ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) by A1; take d = d; ::_thesis: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) assume o,p,b is_collinear ; ::_thesis: ( o,c,d is_collinear & p,c // b,d ) hence ( o,c,d is_collinear & p,c // b,d ) by A2, Def2; ::_thesis: verum end; hence ( o,a,p is_collinear & qtrap o,p ) by Def9; ::_thesis: verum end; theorem Th102: :: SEMI_AF1:102 for SAS being Semi_Affine_Space ex x, y, z being Element of SAS st ( x <> y & y <> z & z <> x ) proof let SAS be Semi_Affine_Space; ::_thesis: ex x, y, z being Element of SAS st ( x <> y & y <> z & z <> x ) consider x, y, z being Element of SAS such that A1: not x,y // x,z by Def1; take x ; ::_thesis: ex y, z being Element of SAS st ( x <> y & y <> z & z <> x ) take y ; ::_thesis: ex z being Element of SAS st ( x <> y & y <> z & z <> x ) take z ; ::_thesis: ( x <> y & y <> z & z <> x ) thus ( x <> y & y <> z & z <> x ) by A1, Def1, Th1, Th3; ::_thesis: verum end; theorem Th103: :: SEMI_AF1:103 for SAS being Semi_Affine_Space for o, p being Element of SAS st qtrap o,p holds o <> p proof let SAS be Semi_Affine_Space; ::_thesis: for o, p being Element of SAS st qtrap o,p holds o <> p let o, p be Element of SAS; ::_thesis: ( qtrap o,p implies o <> p ) ex b being Element of SAS st o <> b proof consider x, y, z being Element of SAS such that A1: x <> y and y <> z and z <> x by Th102; ( o <> x or o <> y or o <> z ) by A1; hence ex b being Element of SAS st o <> b ; ::_thesis: verum end; then consider b being Element of SAS such that A2: o <> b ; consider c being Element of SAS such that A3: not o,b // o,c by A2, Th13; assume qtrap o,p ; ::_thesis: o <> p then consider d being Element of SAS such that A4: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) by Def9; A5: now__::_thesis:_(_b_<>_d_&_not_o,b_//_o,c_&_o,d_//_b,d_&_o,c_//_b,d_implies_(_b_<>_d_&_not_o,b_//_o,c_&_b,d_//_o,b_&_b,d_//_o,c_)_) assume that A6: ( b <> d & not o,b // o,c ) and A7: o,d // b,d and A8: o,c // b,d ; ::_thesis: ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c ) d,o // d,b by A7, Th6; hence ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c ) by A6, A8, Th6, Th7; ::_thesis: verum end; assume not o <> p ; ::_thesis: contradiction then ( o,o // o,b implies ( o,c // o,d & o,c // b,d ) ) by A4, Def2; then ( ( b = d & not o,b // o,c & o,c // o,d ) or ( b <> d & o <> c & not o,b // o,c & o,c // o,d & o,c // b,d ) ) by A3, Def1, Th3; hence contradiction by A5, Def1, Th6; ::_thesis: verum end; theorem :: SEMI_AF1:104 for SAS being Semi_Affine_Space for o, p being Element of SAS st qtrap o,p holds ex q being Element of SAS st ( not o,p,q is_collinear & qtrap o,q ) proof let SAS be Semi_Affine_Space; ::_thesis: for o, p being Element of SAS st qtrap o,p holds ex q being Element of SAS st ( not o,p,q is_collinear & qtrap o,q ) let o, p be Element of SAS; ::_thesis: ( qtrap o,p implies ex q being Element of SAS st ( not o,p,q is_collinear & qtrap o,q ) ) A1: o,p // o,p by Th1; assume A2: qtrap o,p ; ::_thesis: ex q being Element of SAS st ( not o,p,q is_collinear & qtrap o,q ) then A3: o <> p by Th103; consider r being Element of SAS such that A4: not o,p,r is_collinear by A2, Th25, Th103; consider q being Element of SAS such that A5: o,r,q is_collinear and A6: qtrap o,q by Th101; take q ; ::_thesis: ( not o,p,q is_collinear & qtrap o,q ) ( o <> q & o,r // o,q ) by A5, A6, Def2, Th103; hence ( not o,p,q is_collinear & qtrap o,q ) by A3, A4, A6, A1, Th23; ::_thesis: verum end; theorem :: SEMI_AF1:105 for SAS being Semi_Affine_Space for o, p, c, b being Element of SAS st not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p holds ex d being Element of SAS st trap p,b,c,d,o proof let SAS be Semi_Affine_Space; ::_thesis: for o, p, c, b being Element of SAS st not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p holds ex d being Element of SAS st trap p,b,c,d,o let o, p, c, b be Element of SAS; ::_thesis: ( not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p implies ex d being Element of SAS st trap p,b,c,d,o ) assume that A1: ( not o,p,c is_collinear & o,p,b is_collinear ) and A2: qtrap o,p ; ::_thesis: ex d being Element of SAS st trap p,b,c,d,o consider d being Element of SAS such that A3: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) by A2, Def9; take d ; ::_thesis: trap p,b,c,d,o thus trap p,b,c,d,o by A1, A3, Def8; ::_thesis: verum end;