let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds
congr b,c,r,q
let a, b, c, p, q, 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, Th69;
consider s being Element of SAS such that
A4: congr p,q,r,s by Th63;
congr r,p,s,q by A4, Th69;
then A5: congr a,c,s,q by A3, Th65;
congr p,q,b,a by A1;
then congr b,a,r,s by A4, Th65;
hence congr b,c,r,q by A5, Th70; :: thesis: verum