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

now

assume a <> b ; :: thesis: contradiction
then ex p, q being Element of SAS st
( parallelogram p,q,a,b & parallelogram p,q,b,a ) by A1, Def4;
hence contradiction by Th65; :: thesis: verum

end;

hence a = b ; :: thesis: verum