let SAS be Semi_Affine_Space; :: thesis: for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds
x = y
let a, b, c, x, y be Element of SAS; :: thesis: ( congr a,b,c,x & congr a,b,c,y implies x = y )
assume that
A1: congr a,b,c,x and
A2: congr a,b,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, Th59;
hence x = y by Th45; :: 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 SAS such that
A8: parallelogram a,b,p,q by A6, Lm1;
parallelogram p,q,a,b by A8, Th43;
then ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A2, A7, Th61;
hence x = y by Th45; :: thesis: verum
end;
now :: thesis: ( a = b implies x = y )
assume A9: a = b ; :: thesis: x = y
then c = x by A1, Th54;
hence x = y by A2, A9, Th54; :: thesis: verum
end;
hence x = y by A5, A3; :: thesis: verum