let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st a,b // c,d holds
b,a // c,d
let a, b, c, d be Element of SAS; ( a,b // c,d implies b,a // c,d )
assume A1:
a,b // c,d
; b,a // c,d
a,b // b,a
by Def1;
then
( a <> b implies b,a // c,d )
by A1, Def1;
hence
b,a // c,d
by A1; verum