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