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 A1: ( congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b ) ; :: thesis: parallelogram r,s,c,d

now

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

end;

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