theorem Th11: :: BKMODEL1:13

for a, b being Real holds
( (a ^2) + (b ^2) = 1 iff |[a,b]| in circle (0,0,1) )