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

A2: now :: thesis: ( a = c implies congr a,c,b,d )

assume A3: a = c ; :: thesis: congr a,c,b,d
congr a,b,a,b by Th64;
then b = d by A1, A3, Th62;
hence congr a,c,b,d by A3; :: thesis: verum

end;

A4: now :: thesis: ( a <> b & a <> c & a,b,c are_collinear implies congr a,c,b,d )

assume that
A5: a <> b and
A6: a <> c and
A7: a,b,c are_collinear ; :: thesis: congr a,c,b,d
A8: a,b // a,c by A7;
consider p, q being Element of SAS such that
A9: parallelogram p,q,a,b and
A10: parallelogram p,q,c,d by A1, A5;
A11: a,p // a,p by Th1;
( not a,b,p are_collinear & a <> p ) by A9, Th36, Th38;
then consider r being Element of SAS such that
A12: parallelogram a,c,p,r by A6, A8, A11, Th23, Th44;
A13: a,c // p,r by A12;
A14: p,q // c,d by A10;
( p <> q & p,q // a,b ) by A9, Th36;
then A15: a,b // c,d by A14, Def1;
then a,c // b,d by A5, A7, Th32;
then A16: p,r // b,d by A6, A13, Def1;
parallelogram p,r,a,c by A12, Th43;
then A17: p,a // r,c ;
( p,a // q,b & p <> a ) by A9, Th36;
then A18: r,c // q,b by A17, Def1;
p,c // q,d by A10;
then A19: q,d // p,c by Th6;
p,q // a,b by A9;
then A20: a,b // p,q by Th6;
A21: a,c // p,r by A12;
a,b // a,c by A7;
then a,c // p,q by A5, A20, Def1;
then p,q // p,r by A6, A21, Def1;
then A22: r,q // r,p by Th7;
a,c,b are_collinear by A7, Th22;
then A23: not p,r,b are_collinear by A12, Th39;
A24: parallelogram p,r,a,c by A12, Th43;
c,b // c,d by A5, A7, A15, Th33;
then b,c // b,d by Th7;
then p,b // r,d by A22, A18, A19, Def1;
then parallelogram p,r,b,d by A23, A16;
hence congr a,c,b,d by A24; :: thesis: verum

end;

A25: now :: thesis: ( a <> b & a <> c & not a,b,c are_collinear implies congr a,c,b,d )

assume that
a <> b and
a <> c and
A26: not a,b,c are_collinear ; :: thesis: congr a,c,b,d
parallelogram a,b,c,d by A1, A26, Th59;
then parallelogram a,c,b,d by Th43;
hence congr a,c,b,d by Th60; :: thesis: verum

end;

now :: thesis: ( a = b implies congr a,c,b,d )

assume A27: a = b ; :: thesis: congr a,c,b,d
then c = d by A1, Th54;
hence congr a,c,b,d by A27, Th64; :: thesis: verum

end;

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