let FdSp be FanodesSp; :: thesis: for a, b, c being Element of FdSp ex d being Element of FdSp st a,b congr c,d
let a, b, c be Element of FdSp; :: thesis: ex d being Element of FdSp st a,b congr c,d

A1: now

assume a = b ; :: thesis: ex d being Element of FdSp st a,b congr c,d
then a,b congr c,c by Def4;
hence ex d being Element of FdSp st a,b congr c,d ; :: thesis: verum

end;

A2: now

assume A3: ( a <> b & a,b,c is_collinear ) ; :: thesis: ex d being Element of FdSp st a,b congr c,d
then consider p, q being Element of FdSp such that
A4: parallelogram a,b,p,q by Th51;
A5: ( parallelogram p,q,a,b & not p,q,c is_collinear ) by A3, A4, Th37, Th41;
then consider d being Element of FdSp such that
A6: parallelogram p,q,c,d by Th42;
a,b congr c,d by A5, A6, Def4;
hence ex d being Element of FdSp st a,b congr c,d ; :: thesis: verum

end;

now

assume ( a <> b & not a,b,c is_collinear ) ; :: thesis: ex d being Element of FdSp st a,b congr c,d
then consider d being Element of FdSp such that
A7: parallelogram a,b,c,d by Th42;
thus ex d being Element of FdSp st a,b congr c,d by A7, Th61; :: thesis: verum

end;

hence ex d being Element of FdSp st a,b congr c,d by A1, A2; :: thesis: verum