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

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

assume a <> b ; :: thesis: a,b // c,d
then consider p, q being Element of SAS such that
A2: parallelogram p,q,a,b and
A3: parallelogram p,q,c,d by A1;
A4: p,q // c,d by A3;
( p <> q & p,q // a,b ) by A2, Th36;
hence a,b // c,d by A4, Def1; :: thesis: verum

end;

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