let SAS be Semi_Affine_Space; :: thesis: for r, s, a, b, c, d being Element of SAS st congr r,s,a,b & congr r,s,c,d holds
congr a,b,c,d
let r, s, a, b, c, d be Element of SAS; :: thesis: ( congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d )
assume A1: ( congr r,s,a,b & congr r,s,c,d ) ; :: thesis: congr a,b,c,d

A2: now

assume r = s ; :: thesis: congr a,b,c,d
then ( a = b & c = d ) by A1, Th73;
hence congr a,b,c,d by Def4; :: thesis: verum

end;

A3: now

assume A4: ( r <> s & r,s,a is_collinear ) ; :: thesis: congr a,b,c,d
then consider p, q being Element of SAS such that
A5: ( parallelogram p,q,r,s & parallelogram p,q,c,d ) by A1, Def4;
parallelogram p,q,a,b by A1, A4, A5, Th80;
hence congr a,b,c,d by A5, Def4; :: thesis: verum

end;

A6: now

assume A7: ( r <> s & r,s,c is_collinear ) ; :: thesis: congr a,b,c,d
then consider p, q being Element of SAS such that
A8: ( parallelogram p,q,r,s & parallelogram p,q,a,b ) by A1, Def4;
parallelogram p,q,c,d by A1, A7, A8, Th80;
hence congr a,b,c,d by A8, Def4; :: thesis: verum

end;

now

assume ( r <> s & not r,s,a is_collinear & not r,s,c is_collinear ) ; :: thesis: congr a,b,c,d
then ( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, Th78;
hence congr a,b,c,d by Def4; :: thesis: verum

end;

hence congr a,b,c,d by A2, A3, A6; :: thesis: verum