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 that
A1: congr b,a,p,q and
A2: congr c,a,p,r ; :: thesis: congr b,c,r,q
A3: congr r,p,a,c by A2, Th89;
consider s being Element of SAS such that
A4: congr p,q,r,s by Th82;
congr r,p,s,q by A4, Th89;
then A5: congr a,c,s,q by A3, Th85;
congr p,q,b,a by A1, Th89;
then congr b,a,r,s by A4, Th85;
hence congr b,c,r,q by A5, Th90; :: thesis: verum