let FdSp be FanodesSp; :: thesis: for a, b, c, d, r, s being Element of FdSp st a,b congr 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 FdSp; :: thesis: ( a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1: a,b congr c,d and
A2: a,b,c is_collinear and
A3: parallelogram r,s,a,b ; :: thesis: parallelogram r,s,c,d

now

assume A4: a <> b ; :: thesis: parallelogram r,s,c,d
then consider p, q being Element of FdSp such that
A5: parallelogram p,q,a,b and
A6: parallelogram p,q,c,d by A1, Def4;
( r,s '||' a,b & a,b '||' c,d ) by A1, A3, Def3, Th58;
then A7: r,s '||' c,d by A4, PARSP_1:26;
A8: parallelogram a,b,r,s by A3, Th41;
parallelogram a,b,p,q by A5, Th41;
then A9: r,c '||' s,d by A6, A8, Th50;
not r,s,c is_collinear by A2, A3, Th37;
hence parallelogram r,s,c,d by A7, A9, Def3; :: thesis: verum

end;

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