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