let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds
b,c // q,r
let a, b, c, p, q, r be Element of SAS; :: thesis: ( congr b,a,p,q & congr c,a,p,r implies b,c // q,r )
assume ( congr b,a,p,q & congr c,a,p,r ) ; :: thesis: b,c // q,r
then congr b,c,r,q by Th71;
then b,c // r,q by Th57;
hence b,c // q,r by Th6; :: thesis: verum