let AS be AffinSpace; :: thesis: not for x, y, z being Element of AS holds LIN x,y,z
consider x, y, z being Element of AS such that
A1: not x,y // x,z by DIRAF:40;
not LIN x,y,z by A1;
hence not for x, y, z being Element of AS holds LIN x,y,z ; :: thesis: verum