theorem :: BKMODEL4:9

for P being POINT of BK-model-Plane holds T2_to_BK (BK_to_T2 P) = P