let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds
congr a,c,p,s
let a, b, c, p, q, s be Element of SAS; :: thesis: ( congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s )
assume ( congr a,b,p,q & congr b,c,q,s ) ; :: thesis: congr a,c,p,s
then ( congr b,q,a,p & congr b,q,c,s ) by Th69;
then congr a,p,c,s by Th65;
hence congr a,c,p,s by Th68; :: thesis: verum