let SAS be Semi_Affine_Space; :: thesis: for a, b, p, q, c, 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, p, q, c, 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 Th89;
then congr a,p,c,s by Th85;
hence congr a,c,p,s by Th88; :: thesis: verum