theorem Th29: :: BKMODEL4:38

for n31, n32, n33 being Element of F_Real
for u, v being Element of (TOP-REAL 2) st u in inside_of_circle (0,0,1) & v in inside_of_circle (0,0,1) & ( for w being Element of (TOP-REAL 2) st w in inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ) holds
0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)