for u being non zero Element of (TOP-REAL 3) st ((u . 1) ^2) + ((u . 2) ^2) < 1 & u . 3 = 1 holds
Dir u is Element of BK_model