:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation :: by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and :: :: Received October 4, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users 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 proofend; 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 ) ) proofend; Lm3: for AFV being WeakAffVect for a, b, c, d being Element of AFV st a,b '||' c,d holds b,a '||' c,d proofend; Lm4: for AFV being WeakAffVect for a, b being Element of AFV holds a,b '||' b,a proofend; Lm5: for AFV being WeakAffVect for a, b, p being Element of AFV st a,b '||' p,p holds a = b proofend; 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 proofend; Lm7: for AFV being WeakAffVect for a, c being Element of AFV ex b being Element of AFV st a,b '||' b,c proofend; 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 proofend; 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 ) ) ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th5: :: AFVECT01:5 for AFV being WeakAffSegm for a, b being Element of AFV holds a,a // b,b proofend; theorem Th6: :: AFVECT01:6 for AFV being WeakAffSegm for a, b, c being Element of AFV st a,b // c,c holds a = b proofend; 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 proofend; 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 proofend; :: :: RELATION OF MAXIMAL DISTANCE AND MIDPOINT RELATION :: 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 ) proofend; 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 proofend; theorem :: AFVECT01:11 for AFV being WeakAffSegm for a, b being Element of AFV st MDist a,b holds a <> b proofend;