let SAS be Semi_Affine_Space; :: thesis:
let a, b, c, d be Element of SAS; :: thesis:
assume A1: congr a,b,c,d ; :: thesis:

A2: now

assume a = b ; :: thesis:
then ( a = b & c = d ) by A1, Th73;
hence congr a,c,b,d by Th84; :: thesis:

end;

A3: now

assume a = c ; :: thesis:
then ( a = c & congr a,b,a,d & congr a,b,a,b ) by A1, Th84;
then ( a = c & b = d ) by Th81;
hence congr a,c,b,d by Def4; :: thesis:

end;

A4: now

assume A5: ( a <> b & a <> c & a,b,c is_collinear ) ; :: thesis:
then consider p, q being Element of SAS such that
A6: ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4;
( not a,b,p is_collinear & a,b // a,c & a,p // a,p & a <> c & a <> p ) by A5, A6, Def2, Th12, Th54, Th56;
then not a,c,p is_collinear by Th39;
then consider r being Element of SAS such that
A7: parallelogram a,c,p,r by Th62;
A8: parallelogram p,r,a,c by A7, Th61;
a,c,b is_collinear by A5, Th37;
then A9: not p,r,b is_collinear by A7, Th57;
( p <> q & p,q // a,b & p,q // c,d ) by A6, Def3, Th54;
then A10: a,b // c,d by Def1;
then ( a,c // b,d & a,c // p,r & a <> c ) by A5, A7, Def3, Th49;
then A11: p,r // b,d by Def1;
p,q // a,b by A6, Def3;
then ( a <> b & a,b // a,c & a,b // p,q ) by A5, Def2, Th17;
then ( a <> c & a,c // p,q & a,c // p,r ) by A5, A7, Def1, Def3;
then p,q // p,r by Def1;
then A12: r,q // r,p by Th18;
c,b // c,d by A5, A10, Th50;
then A13: b,c // b,d by Th18;
( p,a // r,c & p,a // q,b & p <> a ) by A6, A8, Def3, Th54;
then A14: r,c // q,b by Def1;
p,c // q,d by A6, Def3;
then q,d // p,c by Th17;
then p,b // r,d by A12, A13, A14, Def1;
then ( parallelogram p,r,a,c & parallelogram p,r,b,d ) by A7, A9, A11, Def3, Th61;
hence congr a,c,b,d by Def4; :: thesis:

end;

now

assume ( a <> b & a <> c & not a,b,c is_collinear ) ; :: thesis:
then parallelogram a,b,c,d by A1, Th78;
then parallelogram a,c,b,d by Th61;
hence congr a,c,b,d by Th79; :: thesis:

end;

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