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

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