begin
Lm1:
for r, s, t being Real st r >= 0 & s >= 0 & r + s < t holds
( r < t & s < t )
Lm2:
for r1, r2, r3, r4 being Real holds abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4))
Lm3:
for T being non empty TopSpace
for O being open Subset of T
for A being Subset of T st O meets Cl A holds
O meets A
Lm4:
for T being non empty TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
Cl A c= Cl (union F)
Lm5:
for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete
Lm6:
for T being non empty TopSpace
for U being open Subset of T
for A being Subset of T st A is closed holds
U \ A is open
Lm7:
for r being Real
for A being Point of RealSpace st r > 0 holds
A in Ball (A,r)
Lm8:
for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
Lm9:
for r being Real
for X being non empty set
for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))