let AS be AffinSpace; :: thesis: for a, b being Element of
for A being Subset of st a,b // A holds
b,a // A
let a, b be Element of ; :: thesis: for A being Subset of st a,b // A holds
b,a // A
let A be Subset of ; :: thesis: ( a,b // A implies b,a // A )
assume A1: a,b // A ; :: thesis: b,a // A

now

assume A2: a <> b ; :: thesis: b,a // A
a,b // b,a by Th11;
hence b,a // A by A1, A2, Th46; :: thesis: verum

end;

hence b,a // A by A1; :: thesis: verum