for P, Q being Element of BK_model holds
( P = Q iff BK_to_REAL2 P = BK_to_REAL2 Q )