let AS be AffinSpace; :: thesis: for a, b being Element of AS
for A being Subset of AS st a,b // A holds
b,a // A
let a, b be Element of AS; :: thesis: for A being Subset of AS st a,b // A holds
b,a // A
let A be Subset of AS; :: thesis: ( a,b // A implies b,a // A )
assume A1: a,b // A ; :: thesis: b,a // A
( a <> b implies b,a // A ) by A1, Th1, Th31;
hence b,a // A by A1; :: thesis: verum