let FdSp be FanodesSp; :: thesis: for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y
let a, b, c, x, y be Element of FdSp; :: thesis: ( a,b congr c,x & a,b congr c,y implies x = y )
assume that
A1: a,b congr c,x and
A2: a,b congr c,y ; :: thesis: x = y
A3: now :: thesis: ( a <> b & not a,b,c are_collinear implies x = y )
assume that
a <> b and
A4: not a,b,c are_collinear ; :: thesis: x = y
( parallelogram a,b,c,x & parallelogram a,b,c,y ) by A1, A2, A4, Th50;
hence x = y by Th35; :: thesis: verum
end;
A5: now :: thesis: ( a <> b & a,b,c are_collinear implies x = y )
assume that
A6: a <> b and
A7: a,b,c are_collinear ; :: thesis: x = y
consider p, q being Element of FdSp such that
A8: parallelogram a,b,p,q by A6, Th43;
parallelogram p,q,a,b by A8, Th33;
then ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A2, A7, Th52;
hence x = y by Th35; :: thesis: verum
end;
now :: thesis: ( a = b implies x = y )
assume A9: a = b ; :: thesis: x = y
then c = x by A1, Th45;
hence x = y by A2, A9, Th45; :: thesis: verum
end;
hence x = y by A5, A3; :: thesis: verum