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