let b be Real; :: thesis: for S, T being Element of REAL 2 st |.S.| ^2 <= 1 holds
0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1))
let S, T be Element of REAL 2; :: thesis: ( |.S.| ^2 <= 1 implies 0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1)) )
assume |.S.| ^2 <= 1 ; :: thesis: 0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1))
then (|.S.| ^2) - 1 <= (|.S.| ^2) - (|.S.| ^2) by XREAL_1:10;
then A1: (Sum (sqr S)) - 1 <= 0 by TOPREAL9:5;
0 <= |.(T - S).| ^2 ;
then 0 <= Sum (sqr (T - S)) by TOPREAL9:5;
hence 0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1)) by A1, Lem08; :: thesis: verum