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

A2: now

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

end;

A3: now

assume A4: ( r <> s & r,s,a is_collinear ) ; :: thesis: a,b congr c,d
then consider p, q being Element of FdSp such that
A5: ( parallelogram p,q,r,s & parallelogram p,q,c,d ) by A1, Def4;
parallelogram p,q,a,b by A1, A4, A5, Th62;
hence a,b congr c,d by A5, Def4; :: thesis: verum

end;

A6: now

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

end;

now

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

end;

hence a,b congr c,d by A2, A3, A6; :: thesis: verum