let S be OAffinSpace; :: thesis: not for x, y, z being Element of S holds x,y,z are_collinear
consider x, y, z being Element of S such that
A1: not x,y '||' x,z by Th24;
not x,y,z are_collinear by A1;
hence not for x, y, z being Element of S holds x,y,z are_collinear ; :: thesis: verum