let X be non empty set ; :: thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds

( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )

let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X implies ( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) )

assume A1: f is_a_pseudometric_of X ; :: thesis: ( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) by A2, SEQ_2:def 2; :: thesis: verum

( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )

let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X implies ( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) )

assume A1: f is_a_pseudometric_of X ; :: thesis: ( f is bounded_below & ( for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )

A2: now :: thesis: for A being non empty Subset of X

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

let A be non empty Subset of X; :: thesis: for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

let x be Element of X; :: thesis: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

A3: 0 is LowerBound of (dist (f,x)) .: A

hence ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A3; :: thesis: verum

end;( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

let x be Element of X; :: thesis: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )

A3: 0 is LowerBound of (dist (f,x)) .: A

proof

dom (dist (f,x)) = X
by FUNCT_2:def 1;
let rn be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not rn in (dist (f,x)) .: A or 0 <= rn )

assume rn in (dist (f,x)) .: A ; :: thesis: 0 <= rn

then consider y being object such that

A4: y in dom (dist (f,x)) and

y in A and

A5: rn = (dist (f,x)) . y by FUNCT_1:def 6;

reconsider y = y as Element of X by A4;

f . (x,y) >= 0 by A1, NAGATA_1:29;

hence rn >= 0 by A5, Def2; :: thesis: verum

end;assume rn in (dist (f,x)) .: A ; :: thesis: 0 <= rn

then consider y being object such that

A4: y in dom (dist (f,x)) and

y in A and

A5: rn = (dist (f,x)) . y by FUNCT_1:def 6;

reconsider y = y as Element of X by A4;

f . (x,y) >= 0 by A1, NAGATA_1:29;

hence rn >= 0 by A5, Def2; :: thesis: verum

hence ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A3; :: thesis: verum

now :: thesis: for xy being object st xy in dom f holds

f . xy > - 1

hence
( f is bounded_below & ( for A being non empty Subset of Xf . xy > - 1

let xy be object ; :: thesis: ( xy in dom f implies f . xy > - 1 )

assume xy in dom f ; :: thesis: f . xy > - 1

then consider x, y being object such that

A6: ( x in X & y in X ) and

A7: [x,y] = xy by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of X by A6;

( f . (x,y) >= 0 & 0 > - 1 ) by A1, NAGATA_1:29;

hence f . xy > - 1 by A7; :: thesis: verum

end;assume xy in dom f ; :: thesis: f . xy > - 1

then consider x, y being object such that

A6: ( x in X & y in X ) and

A7: [x,y] = xy by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of X by A6;

( f . (x,y) >= 0 & 0 > - 1 ) by A1, NAGATA_1:29;

hence f . xy > - 1 by A7; :: thesis: verum

for x being Element of X holds

( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) by A2, SEQ_2:def 2; :: thesis: verum