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

now

assume a <> b ; :: thesis: congr a,b,a,b
then consider p, q being Element of SAS such that
A1: parallelogram a,b,p,q by Lm1;
( parallelogram p,q,a,b & 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