theorem Th28: :: BKMODEL3:33

for a, b being Real st (a ^2) + (b ^2) <= 1 holds
Dir |[a,b,1]| in BK_model \/ absolute