theorem Th22: :: BKMODEL2:30

for P being Element of absolute holds (tangent P) /\ absolute = {P}