theorem Th7: :: DIRAF:7
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) by Th6;