theorem :: ANALOAF:25

for AS being non empty AffinStruct holds
( ( ex a, b being Element of AS st a <> b & ( for a, b, c, d, p, q, r, s being Element of AS holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of AS st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of AS ex d being Element of AS st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of AS st p <> b & b,p // p,c holds
ex d being Element of AS st
( a,p // p,d & a,b // c,d ) ) ) iff AS is OAffinSpace ) by Def5, STRUCT_0:def 10;