theorem Th07: :: BKMODEL1:9

for a being Real holds 0 <= a ^2