let SAS be Semi_Affine_Space; :: thesis: for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds
congr b,c,r,q
let b, a, p, q, c, r be Element of SAS; :: thesis: ( congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q )
assume A1: ( congr b,a,p,q & congr c,a,p,r ) ; :: thesis: congr b,c,r,q
consider s being Element of SAS such that
A2: congr p,q,r,s by Th82;
( congr p,q,b,a & congr p,q,r,s & congr r,p,s,q & congr r,p,a,c ) by A1, A2, Th89;
then ( congr b,a,r,s & congr a,c,s,q ) by Th85;
hence congr b,c,r,q by Th90; :: thesis: verum