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