let AS be AffinSpace; 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; for A being Subset of AS st a,b // A holds
b,a // A
let A be Subset of AS; ( a,b // A implies b,a // A )
assume A1:
a,b // A
; b,a // A
( a <> b implies b,a // A )
by A1, Th1, Th31;
hence
b,a // A
by A1; verum