theorem :: BKMODEL2:3

for P being Element of BK_model holds REAL2_to_BK (BK_to_REAL2 P) = P