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 that
A1: trap a,b,c,x,o and
A2: trap a,b,c,y,o ; :: thesis: x = y
A3: ( a,c // b,x & a,c // b,y ) by A1, A2, Def8;
A4: ( not o,a,c is_collinear & o,a,b is_collinear ) by A1, Def8;
( o,c,x is_collinear & o,c,y is_collinear ) by A1, A2, Def8;
hence x = y by A4, A3, Th51; :: thesis: verum