let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d
let a, b, c, d, r, s be Element of SAS; :: thesis: ( congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1: congr a,b,c,d and
A2: a,b,c is_collinear and
A3: parallelogram r,s,a,b ; :: thesis: parallelogram r,s,c,d

now

A4: parallelogram a,b,r,s by A3, Th61;
assume A5: a <> b ; :: thesis: parallelogram r,s,c,d
then consider p, q being Element of SAS such that
A6: parallelogram p,q,a,b and
A7: parallelogram p,q,c,d by A1, Def4;
parallelogram a,b,p,q by A6, Th61;
then A8: r,c // s,d by A7, A4, Th70;
( r,s // a,b & a,b // c,d ) by A1, A3, Def3, Th76;
then A9: r,s // c,d by A5, Th20;
not r,s,c is_collinear by A2, A3, Th57;
hence parallelogram r,s,c,d by A9, A8, Def3; :: thesis: verum

end;

hence parallelogram r,s,c,d by A3, Th54; :: thesis: verum