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 :: thesis: ( a <> b implies congr a,b,a,b )
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 by A1, Th43;
hence congr a,b,a,b ; :: thesis: verum
end;
hence congr a,b,a,b ; :: thesis: verum