let e be Real; :: thesis: for b, c, d being non negative Real st d < e / ((2 * b) * |.c.|) holds
( b is positive & c is positive )
let b, c, d be non negative Real; :: thesis: ( d < e / ((2 * b) * |.c.|) implies ( b is positive & c is positive ) )
assume A1: d < e / ((2 * b) * |.c.|) ; :: thesis: ( b is positive & c is positive )
assume ( not b is positive or not c is positive ) ; :: thesis: contradiction

per cases then ( b <= 0 or c <= 0 ) ;

suppose b <= 0 ; :: thesis: contradiction

then (2 * b) * |.c.| = 0 ;
hence contradiction by A1, XCMPLX_1:49; :: thesis: verum

end;

suppose c <= 0 ; :: thesis: contradiction

then |.c.| = 0 ;
hence contradiction by A1, XCMPLX_1:49; :: thesis: verum

end;

end;