let A, B, C be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) holds
r is positive
let a, b, r be Real; :: thesis: ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) implies r is positive )
assume that
A1: A,B,C is_a_triangle and
A2: ( A in circle (a,b,r) & B in circle (a,b,r) ) ; :: thesis: r is positive
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
assume not r is positive ; :: thesis: contradiction
per cases then ( r < 0 or r = 0 ) ;
suppose r < 0 ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum
end;
suppose r = 0 ; :: thesis: contradiction
then ( A in {|[a,b]|} & B in {|[a,b]|} ) by A2, Thm23;
then ( A = |[a,b]| & B = |[a,b]| ) by TARSKI:def 1;
hence contradiction by A3; :: thesis: verum
end;
end;