let P1, P2 be Element of absolute ; :: thesis: ( tangent P1 = tangent P2 implies P1 = P2 )
assume A1: tangent P1 = tangent P2 ; :: thesis: P1 = P2
( absolute /\ (tangent P1) = {P1} & absolute /\ (tangent P2) = {P2} ) by Th22;
hence P1 = P2 by A1, ZFMISC_1:3; :: thesis: verum