theorem Th23: :: BKMODEL2:31

for P1, P2 being Element of absolute st tangent P1 = tangent P2 holds
P1 = P2