let SAS be Semi_Affine_Space; :: thesis: for a, b being Element of SAS holds a,b // a,b
let a, b be Element of SAS; :: thesis: a,b // a,b
b,a // b,b by Def1;
hence a,b // a,b by Def1; :: thesis: verum