theorem :: DIRAF:12

for S being OAffinSpace
for a, b, c, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d