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

A2: now :: thesis: ( a <> b implies a,c // b,d )

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

end;

now :: thesis: ( a = b implies a,c // b,d )

assume A3: a = b ; :: thesis: a,c // b,d
then c = d by A1, Th54;
hence a,c // b,d by A3, Th1; :: thesis: verum

end;

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