:: AFVECT01 semantic presentation begin registration let A be non empty set ; let C be Relation of [:A,A:]; cluster AffinStruct(# A,C #) -> non empty ; coherence not AffinStruct(# A,C #) is empty ; end; Lm1: for AFV being WeakAffVect for a, b, c being Element of AFV st a,b '||' b,c & a <> c holds a,b // b,c proof let AFV be WeakAffVect; ::_thesis: for a, b, c being Element of AFV st a,b '||' b,c & a <> c holds a,b // b,c let a, b, c be Element of AFV; ::_thesis: ( a,b '||' b,c & a <> c implies a,b // b,c ) assume that A1: a,b '||' b,c and A2: a <> c ; ::_thesis: a,b // b,c not a,b // c,b by A2, AFVECT0:4, AFVECT0:7; hence a,b // b,c by A1, DIRAF:def_4; ::_thesis: verum end; Lm2: for AFV being WeakAffVect for a, b being Element of AFV holds ( a,b // b,a iff ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) proof let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds ( a,b // b,a iff ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) let a, b be Element of AFV; ::_thesis: ( a,b // b,a iff ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) A1: now__::_thesis:_(_ex_p,_q_being_Element_of_AFV_st_ (_a,b_'||'_p,q_&_a,p_'||'_p,b_&_a,q_'||'_q,b_)_implies_a,b_//_b,a_) given p, q being Element of AFV such that A2: a,b '||' p,q and A3: a,p '||' p,b and A4: a,q '||' q,b ; ::_thesis: a,b // b,a now__::_thesis:_(_a_<>_b_implies_a,b_//_b,a_) A5: now__::_thesis:_(_MDist_p,q_implies_a,b_//_b,a_) assume A6: MDist p,q ; ::_thesis: a,b // b,a ( a,b // p,q or a,b // q,p ) by A2, DIRAF:def_4; then MDist a,b by A6, AFVECT0:3, AFVECT0:15; hence a,b // b,a by AFVECT0:def_2; ::_thesis: verum end; assume A7: a <> b ; ::_thesis: a,b // b,a then a,q // q,b by A4, Lm1; then A8: Mid a,q,b by AFVECT0:def_3; A9: now__::_thesis:_not_p_=_q assume p = q ; ::_thesis: contradiction then a,b // p,p by A2, DIRAF:def_4; hence contradiction by A7, AFVECT0:def_1; ::_thesis: verum end; a,p // p,b by A3, A7, Lm1; then Mid a,p,b by AFVECT0:def_3; hence a,b // b,a by A8, A9, A5, AFVECT0:20; ::_thesis: verum end; hence a,b // b,a by AFVECT0:2; ::_thesis: verum end; now__::_thesis:_(_a,b_//_b,a_implies_ex_p,_q_being_Element_of_AFV_st_ (_a,b_'||'_p,q_&_a,p_'||'_p,b_&_a,q_'||'_q,b_)_) assume A10: a,b // b,a ; ::_thesis: ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) A11: now__::_thesis:_(_a_<>_b_implies_ex_p,_q_being_Element_of_AFV_st_ (_a,b_'||'_p,q_&_a,p_'||'_p,b_&_a,q_'||'_q,b_)_) assume a <> b ; ::_thesis: ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) then A12: MDist a,b by A10, AFVECT0:def_2; consider p being Element of AFV such that A13: Mid a,p,b by AFVECT0:19; A14: a,p // p,b by A13, AFVECT0:def_3; consider q being Element of AFV such that A15: a,b // p,q by AFVECT0:def_1; take p = p; ::_thesis: ex q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) take q = q; ::_thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) Mid a,q,b by A13, A15, A12, AFVECT0:15, AFVECT0:23; then a,q // q,b by AFVECT0:def_3; hence ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A15, A14, DIRAF:def_4; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_ex_p,_q_being_Element_of_AFV_st_ (_a,b_'||'_p,q_&_a,p_'||'_p,b_&_a,q_'||'_q,b_)_) assume A16: a = b ; ::_thesis: ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) take p = a; ::_thesis: ex q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) take q = a; ::_thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) a,b // p,q by A16, AFVECT0:2; hence ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A16, DIRAF:def_4; ::_thesis: verum end; hence ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A11; ::_thesis: verum end; hence ( a,b // b,a iff ex p, q being Element of AFV st ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) by A1; ::_thesis: verum end; Lm3: for AFV being WeakAffVect for a, b, c, d being Element of AFV st a,b '||' c,d holds b,a '||' c,d proof let AFV be WeakAffVect; ::_thesis: for a, b, c, d being Element of AFV st a,b '||' c,d holds b,a '||' c,d let a, b, c, d be Element of AFV; ::_thesis: ( a,b '||' c,d implies b,a '||' c,d ) assume a,b '||' c,d ; ::_thesis: b,a '||' c,d then ( a,b // c,d or a,b // d,c ) by DIRAF:def_4; then ( b,a // d,c or b,a // c,d ) by AFVECT0:7; hence b,a '||' c,d by DIRAF:def_4; ::_thesis: verum end; Lm4: for AFV being WeakAffVect for a, b being Element of AFV holds a,b '||' b,a proof let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds a,b '||' b,a let a, b be Element of AFV; ::_thesis: a,b '||' b,a a,b // a,b by AFVECT0:1; hence a,b '||' b,a by DIRAF:def_4; ::_thesis: verum end; Lm5: for AFV being WeakAffVect for a, b, p being Element of AFV st a,b '||' p,p holds a = b proof let AFV be WeakAffVect; ::_thesis: for a, b, p being Element of AFV st a,b '||' p,p holds a = b let a, b, p be Element of AFV; ::_thesis: ( a,b '||' p,p implies a = b ) assume a,b '||' p,p ; ::_thesis: a = b then a,b // p,p by DIRAF:def_4; hence a = b by AFVECT0:def_1; ::_thesis: verum end; Lm6: for AFV being WeakAffVect for a, b, c, d, p, q being Element of AFV st a,b '||' p,q & c,d '||' p,q holds a,b '||' c,d proof let AFV be WeakAffVect; ::_thesis: for a, b, c, d, p, q being Element of AFV st a,b '||' p,q & c,d '||' p,q holds a,b '||' c,d let a, b, c, d, p, q be Element of AFV; ::_thesis: ( a,b '||' p,q & c,d '||' p,q implies a,b '||' c,d ) assume ( a,b '||' p,q & c,d '||' p,q ) ; ::_thesis: a,b '||' c,d then ( ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & c,d // q,p ) or ( a,b // q,p & c,d // p,q ) or ( a,b // q,p & c,d // q,p ) ) by DIRAF:def_4; then ( a,b // c,d or ( a,b // p,q & d,c // p,q ) or ( a,b // q,p & d,c // q,p ) ) by AFVECT0:7, AFVECT0:def_1; then ( a,b // c,d or a,b // d,c ) by AFVECT0:def_1; hence a,b '||' c,d by DIRAF:def_4; ::_thesis: verum end; Lm7: for AFV being WeakAffVect for a, c being Element of AFV ex b being Element of AFV st a,b '||' b,c proof let AFV be WeakAffVect; ::_thesis: for a, c being Element of AFV ex b being Element of AFV st a,b '||' b,c let a, c be Element of AFV; ::_thesis: ex b being Element of AFV st a,b '||' b,c consider b being Element of AFV such that A1: a,b // b,c by AFVECT0:def_1; take b ; ::_thesis: a,b '||' b,c thus a,b '||' b,c by A1, DIRAF:def_4; ::_thesis: verum end; Lm8: for AFV being WeakAffVect for a, a9, b, b9, p being Element of AFV st a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 holds a,b '||' a9,b9 proof let AFV be WeakAffVect; ::_thesis: for a, a9, b, b9, p being Element of AFV st a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 holds a,b '||' a9,b9 let a, a9, b, b9, p be Element of AFV; ::_thesis: ( a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 implies a,b '||' a9,b9 ) assume that A1: a <> a9 and A2: b <> b9 and A3: p,a '||' p,a9 and A4: p,b '||' p,b9 ; ::_thesis: a,b '||' a9,b9 b,p // p,b9 by A2, A4, Lm1, Lm3; then A5: Mid b,p,b9 by AFVECT0:def_3; a,p // p,a9 by A1, A3, Lm1, Lm3; then Mid a,p,a9 by AFVECT0:def_3; then a,b // b9,a9 by A5, AFVECT0:25; hence a,b '||' a9,b9 by DIRAF:def_4; ::_thesis: verum end; Lm9: for AFV being WeakAffVect for a, b being Element of AFV holds ( a = b or ex c being Element of AFV st ( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) ) proof let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds ( a = b or ex c being Element of AFV st ( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) ) let a, b be Element of AFV; ::_thesis: ( a = b or ex c being Element of AFV st ( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) ) consider c being Element of AFV such that A1: a,b // b,c by AFVECT0:def_1; A2: now__::_thesis:_(_not_a_=_c_or_a_=_b_or_ex_p,_p9_being_Element_of_AFV_st_ (_p_<>_p9_&_a,b_'||'_p,p9_&_a,p_'||'_p,b_&_a,p9_'||'_p9,b_)_) assume a = c ; ::_thesis: ( a = b or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) then consider p, p9 being Element of AFV such that A3: a,b '||' p,p9 and A4: ( a,p '||' p,b & a,p9 '||' p9,b ) by A1, Lm2; ( p = p9 implies a = b ) by A3, Lm5; hence ( a = b or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) by A3, A4; ::_thesis: verum end; now__::_thesis:_(_a_<>_c_implies_ex_c_being_Element_of_AFV_st_ (_a_<>_c_&_a,b_'||'_b,c_)_) assume A5: a <> c ; ::_thesis: ex c being Element of AFV st ( a <> c & a,b '||' b,c ) a,b '||' b,c by A1, DIRAF:def_4; hence ex c being Element of AFV st ( a <> c & a,b '||' b,c ) by A5; ::_thesis: verum end; hence ( a = b or ex c being Element of AFV st ( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st ( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) ) by A2; ::_thesis: verum end; Lm10: for AFV being WeakAffVect for a, b, b9, p, p9, c being Element of AFV st a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 holds a,b9 '||' b9,c proof let AFV be WeakAffVect; ::_thesis: for a, b, b9, p, p9, c being Element of AFV st a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 holds a,b9 '||' b9,c let a, b, b9, p, p9, c be Element of AFV; ::_thesis: ( a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 implies a,b9 '||' b9,c ) assume that A1: a,b '||' b,c and A2: ( b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) ; ::_thesis: a,b9 '||' b9,c A3: b,b9 // b9,b by A2, Lm2; A4: now__::_thesis:_(_a,b_//_b,c_implies_a,b9_'||'_b9,c_) assume A5: a,b // b,c ; ::_thesis: a,b9 '||' b9,c then A6: Mid a,b,c by AFVECT0:def_3; A7: now__::_thesis:_(_MDist_b,b9_implies_a,b9_'||'_b9,c_) assume MDist b,b9 ; ::_thesis: a,b9 '||' b9,c then Mid a,b9,c by A6, AFVECT0:23; then a,b9 // b9,c by AFVECT0:def_3; hence a,b9 '||' b9,c by DIRAF:def_4; ::_thesis: verum end; ( b = b9 implies a,b9 '||' b9,c ) by A5, DIRAF:def_4; hence a,b9 '||' b9,c by A3, A7, AFVECT0:def_2; ::_thesis: verum end; now__::_thesis:_(_a,b_//_c,b_implies_a,b9_'||'_b9,c_) assume a,b // c,b ; ::_thesis: a,b9 '||' b9,c then a = c by AFVECT0:4, AFVECT0:7; then a,b9 // c,b9 by AFVECT0:1; hence a,b9 '||' b9,c by DIRAF:def_4; ::_thesis: verum end; hence a,b9 '||' b9,c by A1, A4, DIRAF:def_4; ::_thesis: verum end; Lm11: for AFV being WeakAffVect for a, b, b9, c being Element of AFV st a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c holds ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) proof let AFV be WeakAffVect; ::_thesis: for a, b, b9, c being Element of AFV st a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c holds ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) let a, b, b9, c be Element of AFV; ::_thesis: ( a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c implies ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) ) assume that A1: a <> c and A2: b <> b9 and A3: a,b '||' b,c and A4: a,b9 '||' b9,c ; ::_thesis: ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) a,b9 // b9,c by A1, A4, Lm1; then A5: Mid a,b9,c by AFVECT0:def_3; a,b // b,c by A1, A3, Lm1; then Mid a,b,c by AFVECT0:def_3; then MDist b,b9 by A2, A5, AFVECT0:20; then b,b9 // b9,b by AFVECT0:def_2; then consider p, p9 being Element of AFV such that A6: b,b9 '||' p,p9 and A7: ( b,p '||' p,b9 & b,p9 '||' p9,b9 ) by Lm2; ( p <> p9 implies ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) ) by A6, A7; hence ex p, p9 being Element of AFV st ( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) by A2, A6, Lm5; ::_thesis: verum end; Lm12: for AFV being WeakAffVect for a, b, c, p, p9, q, q9 being Element of AFV st a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c holds ex r, r9 being Element of AFV st ( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) proof let AFV be WeakAffVect; ::_thesis: for a, b, c, p, p9, q, q9 being Element of AFV st a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c holds ex r, r9 being Element of AFV st ( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) let a, b, c, p, p9, q, q9 be Element of AFV; ::_thesis: ( a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c implies ex r, r9 being Element of AFV st ( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) ) assume ( a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c ) ; ::_thesis: ex r, r9 being Element of AFV st ( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) then ( a,b // b,a & a,c // c,a ) by Lm2; then b,c // c,b by AFVECT0:12; hence ex r, r9 being Element of AFV st ( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) by Lm2; ::_thesis: verum end; set AFV0 = the WeakAffVect; set X = the carrier of the WeakAffVect; set XX = [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:]; defpred S1[ set , set ] means ex a, b, c, d being Element of the carrier of the WeakAffVect st ( $1 = [a,b] & $2 = [c,d] & a,b '||' c,d ); consider P being Relation of [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:],[: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] such that Lm13: for x, y being set holds ( [x,y] in P iff ( x in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & y in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & S1[x,y] ) ) from RELSET_1:sch_1(); Lm14: for a, b, c, d being Element of the carrier of the WeakAffVect holds ( [[a,b],[c,d]] in P iff a,b '||' c,d ) proof let a, b, c, d be Element of the carrier of the WeakAffVect; ::_thesis: ( [[a,b],[c,d]] in P iff a,b '||' c,d ) A1: ( [[a,b],[c,d]] in P implies a,b '||' c,d ) proof assume [[a,b],[c,d]] in P ; ::_thesis: a,b '||' c,d then consider a9, b9, c9, d9 being Element of the carrier of the WeakAffVect such that A2: [a,b] = [a9,b9] and A3: [c,d] = [c9,d9] and A4: a9,b9 '||' c9,d9 by Lm13; A5: c = c9 by A3, XTUPLE_0:1; ( a = a9 & b = b9 ) by A2, XTUPLE_0:1; hence a,b '||' c,d by A3, A4, A5, XTUPLE_0:1; ::_thesis: verum end; ( [a,b] in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & [c,d] in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] ) by ZFMISC_1:def_2; hence ( [[a,b],[c,d]] in P iff a,b '||' c,d ) by A1, Lm13; ::_thesis: verum end; set WAS = AffinStruct(# the carrier of the WeakAffVect,P #); Lm15: for a, b, c, d being Element of the WeakAffVect for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a = a9 & b = b9 & c = c9 & d = d9 holds ( a,b '||' c,d iff a9,b9 // c9,d9 ) proof let a, b, c, d be Element of the WeakAffVect; ::_thesis: for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a = a9 & b = b9 & c = c9 & d = d9 holds ( a,b '||' c,d iff a9,b9 // c9,d9 ) let a9, b9, c9, d9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b '||' c,d iff a9,b9 // c9,d9 ) ) assume A1: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; ::_thesis: ( a,b '||' c,d iff a9,b9 // c9,d9 ) A2: now__::_thesis:_(_a9,b9_//_c9,d9_implies_a,b_'||'_c,d_) assume a9,b9 // c9,d9 ; ::_thesis: a,b '||' c,d then [[a9,b9],[c9,d9]] in P by ANALOAF:def_2; hence a,b '||' c,d by A1, Lm14; ::_thesis: verum end; now__::_thesis:_(_a,b_'||'_c,d_implies_a9,b9_//_c9,d9_) assume a,b '||' c,d ; ::_thesis: a9,b9 // c9,d9 then [[a,b],[c,d]] in the CONGR of AffinStruct(# the carrier of the WeakAffVect,P #) by Lm14; hence a9,b9 // c9,d9 by A1, ANALOAF:def_2; ::_thesis: verum end; hence ( a,b '||' c,d iff a9,b9 // c9,d9 ) by A2; ::_thesis: verum end; Lm16: now__::_thesis:_(_ex_a9,_b9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a9_<>_b9_&_(_for_a9,_b9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_holds_a9,b9_//_b9,a9_)_&_(_for_a9,_b9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a9,b9_//_a9,a9_holds_ a9_=_b9_)_&_(_for_a,_b,_c,_d,_p,_q_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a,b_//_p,q_&_c,d_//_p,q_holds_ a,b_//_c,d_)_&_(_for_a,_c_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_ex_b_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a,b_//_b,c_)_&_(_for_a,_a9,_b,_b9,_p_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a_<>_a9_&_b_<>_b9_&_p,a_//_p,a9_&_p,b_//_p,b9_holds_ a,b_//_a9,b9_)_&_(_for_a,_b_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_holds_ (_a_=_b_or_ex_c_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_(_a_<>_c_&_a,b_//_b,c_)_or_ex_p,_p9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_p_<>_p9_&_a,b_//_p,p9_&_a,p_//_p,b_&_a,p9_//_p9,b_)_)_)_)_&_(_for_a,_b,_b9,_p,_p9,_c_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a,b_//_b,c_&_b,b9_//_p,p9_&_b,p_//_p,b9_&_b,p9_//_p9,b9_holds_ a,b9_//_b9,c_)_&_(_for_a,_b,_b9,_c_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a_<>_c_&_b_<>_b9_&_a,b_//_b,c_&_a,b9_//_b9,c_holds_ ex_p,_p9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_p_<>_p9_&_b,b9_//_p,p9_&_b,p_//_p,b9_&_b,p9_//_p9,b9_)_)_&_(_for_a,_b,_c,_p,_p9,_q,_q9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_a,b_//_p,p9_&_a,c_//_q,q9_&_a,p_//_p,b_&_a,q_//_q,c_&_a,p9_//_p9,b_&_a,q9_//_q9,c_holds_ ex_r,_r9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_b,c_//_r,r9_&_b,r_//_r,c_&_b,r9_//_r9,c_)_)_) thus ex a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9 <> b9 by STRUCT_0:def_10; ::_thesis: ( ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds a9,b9 // b9,a9 ) & ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds a9 = b9 ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) thus for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds a9,b9 // b9,a9 ::_thesis: ( ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds a9 = b9 ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a9, b9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: a9,b9 // b9,a9 reconsider a = a9, b = b9 as Element of the WeakAffVect ; a,b '||' b,a by Lm4; hence a9,b9 // b9,a9 by Lm15; ::_thesis: verum end; thus for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds a9 = b9 ::_thesis: ( ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a9, b9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a9,b9 // a9,a9 implies a9 = b9 ) assume A1: a9,b9 // a9,a9 ; ::_thesis: a9 = b9 reconsider a = a9, b = b9 as Element of the WeakAffVect ; a,b '||' a,a by A1, Lm15; hence a9 = b9 by Lm5; ::_thesis: verum end; thus for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds a,b // c,d ::_thesis: ( ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a, b, c, d, p, q be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a,b // p,q & c,d // p,q implies a,b // c,d ) assume A2: ( a,b // p,q & c,d // p,q ) ; ::_thesis: a,b // c,d reconsider a1 = a, b1 = b, c1 = c, d1 = d, p1 = p, q1 = q as Element of the WeakAffVect ; ( a1,b1 '||' p1,q1 & c1,d1 '||' p1,q1 ) by A2, Lm15; then a1,b1 '||' c1,d1 by Lm6; hence a,b // c,d by Lm15; ::_thesis: verum end; thus for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ::_thesis: ( ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c reconsider a1 = a, c1 = c as Element of the WeakAffVect ; consider b1 being Element of the WeakAffVect such that A3: a1,b1 '||' b1,c1 by Lm7; reconsider b = b1 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ; a,b // b,c by A3, Lm15; hence ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ; ::_thesis: verum end; thus for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ::_thesis: ( ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a, a9, b, b9, p be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 implies a,b // a9,b9 ) assume that A4: ( a <> a9 & b <> b9 ) and A5: ( p,a // p,a9 & p,b // p,b9 ) ; ::_thesis: a,b // a9,b9 reconsider a1 = a, a19 = a9, b1 = b, b19 = b9, p1 = p as Element of the WeakAffVect ; ( p1,a1 '||' p1,a19 & p1,b1 '||' p1,b19 ) by A5, Lm15; then a1,b1 '||' a19,b19 by A4, Lm8; hence a,b // a9,b9 by Lm15; ::_thesis: verum end; thus for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ::_thesis: ( ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a, b be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) assume A6: not a = b ; ::_thesis: ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) reconsider a1 = a, b1 = b as Element of the WeakAffVect ; A7: now__::_thesis:_(_ex_p1,_p19_being_Element_of_the_WeakAffVect_st_ (_p1_<>_p19_&_a1,b1_'||'_p1,p19_&_a1,p1_'||'_p1,b1_&_a1,p19_'||'_p19,b1_)_implies_ex_p,_p9_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_p_<>_p9_&_a,b_//_p,p9_&_a,p_//_p,b_&_a,p9_//_p9,b_)_) given p1, p19 being Element of the WeakAffVect such that A8: p1 <> p19 and A9: ( a1,b1 '||' p1,p19 & a1,p1 '||' p1,b1 ) and A10: a1,p19 '||' p19,b1 ; ::_thesis: ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) reconsider p = p1, p9 = p19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ; A11: a,p9 // p9,b by A10, Lm15; ( a,b // p,p9 & a,p // p,b ) by A9, Lm15; hence ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by A8, A11; ::_thesis: verum end; now__::_thesis:_(_ex_c1_being_Element_of_the_WeakAffVect_st_ (_a1_<>_c1_&_a1,b1_'||'_b1,c1_)_implies_ex_c_being_Element_of_AffinStruct(#_the_carrier_of_the_WeakAffVect,P_#)_st_ (_a_<>_c_&_a,b_//_b,c_)_) given c1 being Element of the WeakAffVect such that A12: a1 <> c1 and A13: a1,b1 '||' b1,c1 ; ::_thesis: ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( a <> c & a,b // b,c ) reconsider c = c1 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ; a,b // b,c by A13, Lm15; hence ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( a <> c & a,b // b,c ) by A12; ::_thesis: verum end; hence ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) by A6, A7, Lm9; ::_thesis: verum end; thus for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ::_thesis: ( ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) proof let a, b, b9, p, p9, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 implies a,b9 // b9,c ) assume that A14: ( a,b // b,c & b,b9 // p,p9 ) and A15: ( b,p // p,b9 & b,p9 // p9,b9 ) ; ::_thesis: a,b9 // b9,c reconsider a1 = a, b1 = b, b19 = b9, p1 = p, p19 = p9, c1 = c as Element of the WeakAffVect ; A16: ( b1,p1 '||' p1,b19 & b1,p19 '||' p19,b19 ) by A15, Lm15; ( a1,b1 '||' b1,c1 & b1,b19 '||' p1,p19 ) by A14, Lm15; then a1,b19 '||' b19,c1 by A16, Lm10; hence a,b9 // b9,c by Lm15; ::_thesis: verum end; thus for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ::_thesis: for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) proof let a, b, b9, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c implies ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) assume that A17: ( a <> c & b <> b9 ) and A18: ( a,b // b,c & a,b9 // b9,c ) ; ::_thesis: ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) reconsider a1 = a, b1 = b, b19 = b9, c1 = c as Element of the WeakAffVect ; ( a1,b1 '||' b1,c1 & a1,b19 '||' b19,c1 ) by A18, Lm15; then consider p1, p19 being Element of the WeakAffVect such that A19: p1 <> p19 and A20: ( b1,b19 '||' p1,p19 & b1,p1 '||' p1,b19 ) and A21: b1,p19 '||' p19,b19 by A17, Lm11; reconsider p = p1, p9 = p19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ; A22: b,p9 // p9,b9 by A21, Lm15; ( b,b9 // p,p9 & b,p // p,b9 ) by A20, Lm15; hence ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) by A19, A22; ::_thesis: verum end; thus for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ::_thesis: verum proof let a, b, c, p, p9, q, q9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); ::_thesis: ( a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c implies ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) assume that A23: ( a,b // p,p9 & a,c // q,q9 ) and A24: ( a,p // p,b & a,q // q,c ) and A25: ( a,p9 // p9,b & a,q9 // q9,c ) ; ::_thesis: ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) reconsider a1 = a, b1 = b, c1 = c, p1 = p, p19 = p9, q1 = q, q19 = q9 as Element of the WeakAffVect ; A26: ( a1,p1 '||' p1,b1 & a1,q1 '||' q1,c1 ) by A24, Lm15; A27: ( a1,p19 '||' p19,b1 & a1,q19 '||' q19,c1 ) by A25, Lm15; ( a1,b1 '||' p1,p19 & a1,c1 '||' q1,q19 ) by A23, Lm15; then consider r1, r19 being Element of the WeakAffVect such that A28: ( b1,c1 '||' r1,r19 & b1,r1 '||' r1,c1 ) and A29: b1,r19 '||' r19,c1 by A26, A27, Lm12; reconsider r = r1, r9 = r19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ; A30: b,r9 // r9,c by A29, Lm15; ( b,c // r,r9 & b,r // r,c ) by A28, Lm15; hence ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) by A30; ::_thesis: verum end; end; definition let IT be non empty AffinStruct ; attrIT is WeakAffSegm-like means :Def1: :: AFVECT01:def 1 ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a9, b, b9, p being Element of IT st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of IT holds ( a = b or ex c being Element of IT st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of IT st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of IT st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of IT st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of IT st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of IT st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ); end; :: deftheorem Def1 defines WeakAffSegm-like AFVECT01:def_1_:_ for IT being non empty AffinStruct holds ( IT is WeakAffSegm-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a9, b, b9, p being Element of IT st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds a,b // a9,b9 ) & ( for a, b being Element of IT holds ( a = b or ex c being Element of IT st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of IT st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of IT st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds a,b9 // b9,c ) & ( for a, b, b9, c being Element of IT st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds ex p, p9 being Element of IT st ( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds ex r, r9 being Element of IT st ( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) ); registration cluster non empty non trivial strict WeakAffSegm-like for AffinStruct ; existence ex b1 being non trivial AffinStruct st ( b1 is strict & b1 is WeakAffSegm-like ) proof ( AffinStruct(# the carrier of the WeakAffVect,P #) is WeakAffSegm-like & not AffinStruct(# the carrier of the WeakAffVect,P #) is trivial ) by Def1, Lm16; hence ex b1 being non trivial AffinStruct st ( b1 is strict & b1 is WeakAffSegm-like ) ; ::_thesis: verum end; end; definition mode WeakAffSegm is non trivial WeakAffSegm-like AffinStruct ; end; theorem Th1: :: AFVECT01:1 for AFV being WeakAffSegm for a, b being Element of AFV holds a,b // a,b proof let AFV be WeakAffSegm; ::_thesis: for a, b being Element of AFV holds a,b // a,b let a, b be Element of AFV; ::_thesis: a,b // a,b a,b // b,a by Def1; hence a,b // a,b by Def1; ::_thesis: verum end; theorem Th2: :: AFVECT01:2 for AFV being WeakAffSegm for a, b, c, d being Element of AFV st a,b // c,d holds c,d // a,b proof let AFV be WeakAffSegm; ::_thesis: for a, b, c, d being Element of AFV st a,b // c,d holds c,d // a,b let a, b, c, d be Element of AFV; ::_thesis: ( a,b // c,d implies c,d // a,b ) assume A1: a,b // c,d ; ::_thesis: c,d // a,b c,d // c,d by Th1; hence c,d // a,b by A1, Def1; ::_thesis: verum end; theorem Th3: :: AFVECT01:3 for AFV being WeakAffSegm for a, b, c, d being Element of AFV st a,b // c,d holds a,b // d,c proof let AFV be WeakAffSegm; ::_thesis: for a, b, c, d being Element of AFV st a,b // c,d holds a,b // d,c let a, b, c, d be Element of AFV; ::_thesis: ( a,b // c,d implies a,b // d,c ) assume A1: a,b // c,d ; ::_thesis: a,b // d,c d,c // c,d by Def1; hence a,b // d,c by A1, Def1; ::_thesis: verum end; theorem Th4: :: AFVECT01:4 for AFV being WeakAffSegm for a, b, c, d being Element of AFV st a,b // c,d holds b,a // c,d proof let AFV be WeakAffSegm; ::_thesis: for a, b, c, d being Element of AFV st a,b // c,d holds b,a // c,d let a, b, c, d be Element of AFV; ::_thesis: ( a,b // c,d implies b,a // c,d ) assume a,b // c,d ; ::_thesis: b,a // c,d then c,d // a,b by Th2; then c,d // b,a by Th3; hence b,a // c,d by Th2; ::_thesis: verum end; theorem Th5: :: AFVECT01:5 for AFV being WeakAffSegm for a, b being Element of AFV holds a,a // b,b proof let AFV be WeakAffSegm; ::_thesis: for a, b being Element of AFV holds a,a // b,b let a, b be Element of AFV; ::_thesis: a,a // b,b now__::_thesis:_(_a_<>_b_implies_a,a_//_b,b_) consider c being Element of AFV such that A1: a,c // c,b by Def1; assume A2: a <> b ; ::_thesis: a,a // b,b c,a // c,b by A1, Th4; hence a,a // b,b by A2, Def1; ::_thesis: verum end; hence a,a // b,b by Def1; ::_thesis: verum end; theorem Th6: :: AFVECT01:6 for AFV being WeakAffSegm for a, b, c being Element of AFV st a,b // c,c holds a = b proof let AFV be WeakAffSegm; ::_thesis: for a, b, c being Element of AFV st a,b // c,c holds a = b let a, b, c be Element of AFV; ::_thesis: ( a,b // c,c implies a = b ) assume A1: a,b // c,c ; ::_thesis: a = b a,a // c,c by Th5; then a,b // a,a by A1, Def1; hence a = b by Def1; ::_thesis: verum end; theorem Th7: :: AFVECT01:7 for AFV being WeakAffSegm for a, b, p, p9, c being Element of AFV st a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b holds a = c proof let AFV be WeakAffSegm; ::_thesis: for a, b, p, p9, c being Element of AFV st a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b holds a = c let a, b, p, p9, c be Element of AFV; ::_thesis: ( a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b implies a = c ) assume that A1: a,b // p,p9 and A2: a,b // b,c and A3: a,p // p,b and A4: a,p9 // p9,b ; ::_thesis: a = c p,b // a,p by A3, Th2; then p,b // p,a by Th3; then A5: b,p // p,a by Th4; p9,b // a,p9 by A4, Th2; then p9,b // p9,a by Th3; then A6: b,p9 // p9,a by Th4; b,a // p,p9 by A1, Th4; then a,a // a,c by A2, A5, A6, Def1; then a,c // a,a by Th2; hence a = c by Def1; ::_thesis: verum end; theorem :: AFVECT01:8 for AFV being WeakAffSegm for a, b9, b99, b being Element of AFV st a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 holds b9 = b99 proof let AFV be WeakAffSegm; ::_thesis: for a, b9, b99, b being Element of AFV st a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 holds b9 = b99 let a, b9, b99, b be Element of AFV; ::_thesis: ( a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 implies b9 = b99 ) assume A1: ( a,b9 // a,b99 & a,b // a,b99 ) ; ::_thesis: ( b = b9 or b = b99 or b9 = b99 ) now__::_thesis:_(_b9_<>_b99_&_b_<>_b99_&_not_b_=_b9_&_not_b_=_b99_implies_b9_=_b99_) assume ( b9 <> b99 & b <> b99 ) ; ::_thesis: ( b = b9 or b = b99 or b9 = b99 ) then b9,b // b99,b99 by A1, Def1; hence ( b = b9 or b = b99 or b9 = b99 ) by Th6; ::_thesis: verum end; hence ( b = b9 or b = b99 or b9 = b99 ) ; ::_thesis: verum end; definition let AFV be WeakAffSegm; let a, b be Element of AFV; pred MDist a,b means :Def2: :: AFVECT01:def 2 ex p, p9 being Element of AFV st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ); end; :: deftheorem Def2 defines MDist AFVECT01:def_2_:_ for AFV being WeakAffSegm for a, b being Element of AFV holds ( MDist a,b iff ex p, p9 being Element of AFV st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ); definition let AFV be WeakAffSegm; let a, b, c be Element of AFV; pred Mid a,b,c means :: AFVECT01:def 3 ( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) ); end; :: deftheorem defines Mid AFVECT01:def_3_:_ for AFV being WeakAffSegm for a, b, c being Element of AFV holds ( Mid a,b,c iff ( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) ) ); theorem :: AFVECT01:9 for AFV being WeakAffSegm for a, b being Element of AFV st a <> b & not MDist a,b holds ex c being Element of AFV st ( a <> c & a,b // b,c ) proof let AFV be WeakAffSegm; ::_thesis: for a, b being Element of AFV st a <> b & not MDist a,b holds ex c being Element of AFV st ( a <> c & a,b // b,c ) let a, b be Element of AFV; ::_thesis: ( a <> b & not MDist a,b implies ex c being Element of AFV st ( a <> c & a,b // b,c ) ) assume A1: ( a <> b & not MDist a,b ) ; ::_thesis: ex c being Element of AFV st ( a <> c & a,b // b,c ) ( a = b or ex c being Element of AFV st ( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AFV st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) by Def1; hence ex c being Element of AFV st ( a <> c & a,b // b,c ) by A1, Def2; ::_thesis: verum end; theorem :: AFVECT01:10 for AFV being WeakAffSegm for a, b, c being Element of AFV st MDist a,b & a,b // b,c holds a = c proof let AFV be WeakAffSegm; ::_thesis: for a, b, c being Element of AFV st MDist a,b & a,b // b,c holds a = c let a, b, c be Element of AFV; ::_thesis: ( MDist a,b & a,b // b,c implies a = c ) assume that A1: MDist a,b and A2: a,b // b,c ; ::_thesis: a = c ex p, p9 being Element of AFV st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by A1, Def2; hence a = c by A2, Th7; ::_thesis: verum end; theorem :: AFVECT01:11 for AFV being WeakAffSegm for a, b being Element of AFV st MDist a,b holds a <> b proof let AFV be WeakAffSegm; ::_thesis: for a, b being Element of AFV st MDist a,b holds a <> b let a, b be Element of AFV; ::_thesis: ( MDist a,b implies a <> b ) assume MDist a,b ; ::_thesis: a <> b then ex p, p9 being Element of AFV st ( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by Def2; hence a <> b by Th2, Th6; ::_thesis: verum end;