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

A2: now

assume a <> b ; :: thesis: congr b,a,d,c
then consider p, q being Element of SAS such that
A3: ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4;
( parallelogram q,p,b,a & parallelogram q,p,d,c ) by A3, Th61;
hence congr b,a,d,c by Def4; :: thesis: verum

end;

now

assume A4: a = b ; :: thesis: congr b,a,d,c
then c = d by A1, Th73;
hence congr b,a,d,c by A4, Def4; :: thesis: verum

end;

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