:: 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 ) ) ) );