let AS be AffinSpace; :: thesis: for a being Element of AS ex b being Element of AS st a <> b
let a be Element of AS; :: thesis: ex b being Element of AS st a <> b
consider x, y being Element of AS such that
A1: x <> y by DIRAF:40;
( a = x implies a <> y ) by A1;
hence ex b being Element of AS st a <> b ; :: thesis: verum