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

A3: now

assume that
r <> s and
A4: ( not r,s,a is_collinear & not r,s,c is_collinear ) ; :: thesis: a,b congr c,d
( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, A2, A4, Th60;
hence a,b congr c,d by Def4; :: thesis: verum

end;

A5: now

assume that
A6: r <> s and
A7: r,s,c is_collinear ; :: thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A8: parallelogram p,q,r,s and
A9: parallelogram p,q,a,b by A1, A6, Def4;
parallelogram p,q,c,d by A2, A7, A8, Th62;
hence a,b congr c,d by A9, Def4; :: thesis: verum

end;

A10: now

assume that
A11: r <> s and
A12: r,s,a is_collinear ; :: thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2, A11, Def4;
parallelogram p,q,a,b by A1, A12, A13, Th62;
hence a,b congr c,d by A14, Def4; :: thesis: verum

end;

now

assume r = s ; :: thesis: a,b congr c,d
then ( a = b & c = d ) by A1, A2, Th55;
hence a,b congr c,d by Def4; :: thesis: verum

end;

hence a,b congr c,d by A10, A5, A3; :: thesis: verum