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