let AS be AffinSpace; :: thesis: for a, b being Element of AS st a <> b holds
a,b // Line (a,b)
let a, b be Element of AS; :: thesis: ( a <> b implies a,b // Line (a,b) )
assume A1: a <> b ; :: thesis: a,b // Line (a,b)
a,b // a,b by Th11;
hence a,b // Line (a,b) by A1, Def4; :: thesis: verum