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 that
A1: congr r,s,a,b and
A2: congr r,s,c,d ; :: thesis: congr a,b,c,d

A3: now

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

end;

A5: now

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

end;

A10: now

assume that
A11: r <> s and
A12: r,s,a is_collinear ; :: thesis: congr a,b,c,d
consider p, q being Element of SAS such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2, A11, Def4;
parallelogram p,q,a,b by A1, A12, A13, Th80;
hence congr a,b,c,d by A14, Def4; :: thesis: verum

end;

now

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

end;

hence congr a,b,c,d by A10, A5, A3; :: thesis: verum