let SAS be Semi_Affine_Space; :: thesis: for a, b being Element of holds congr a,b,a,b
let a, b be Element of ; :: thesis: congr a,b,a,b

now

assume a <> b ; :: thesis: congr a,b,a,b
then consider p, q being Element of such that
A1: parallelogram a,b,p,q by Lm1;
parallelogram p,q,a,b by A1, Th61;
hence congr a,b,a,b by Def4; :: thesis: verum

end;

hence congr a,b,a,b by Def4; :: thesis: verum