let r be positive Real; :: thesis: for u being Element of (TOP-REAL 2) st u in circle (0,0,r) holds
not u is zero
let u be Element of (TOP-REAL 2); :: thesis: ( u in circle (0,0,r) implies not u is zero )
assume A1: u in circle (0,0,r) ; :: thesis: not u is zero
assume u is zero ; :: thesis: contradiction
then r ^2 = 0 by A1, BKMODEL1:14, EUCLID:54, Lem01;
hence contradiction ; :: thesis: verum