theorem Th12: :: BKMODEL1:14

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