let SAS be Semi_Affine_Space; :: thesis: for b, a, p, q, c, r being Element of st congr b,a,p,q & congr c,a,p,r holds
b,c // q,r
let b, a, p, q, c, r be Element of ; :: 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 b,c // r,q by Th76, Th91;
hence b,c // q,r by Th17; :: thesis: verum