let SAS be Semi_Affine_Space; :: thesis: for a, b, c, x, o, y being Element of SAS st trap a,b,c,x,o & trap a,b,c,y,o holds
x = y
let a, b, c, x, o, y be Element of SAS; :: thesis: ( trap a,b,c,x,o & trap a,b,c,y,o implies x = y )
assume ( trap a,b,c,x,o & trap a,b,c,y,o ) ; :: thesis: x = y
then ( not o,a,c is_collinear & o,a,b is_collinear & o,c,x is_collinear & o,c,y is_collinear & a,c // b,x & a,c // b,y ) by Def8;
hence x = y by Th51; :: thesis: verum