consider x being object such that
A1: x in the carrier of M by XBOOLE_0:def 1;
reconsider x = x as Point of M by A1;
reconsider X = {x} as Subset of M ;
take S = NAT --> X; :: thesis: ( S is pointwise_bounded & S is non-empty )
A2: now :: thesis: for x1, x2 being Point of M st x1 in X & x2 in X holds
dist (x1,x2) <= 1
let x1, x2 be Point of M; :: thesis: ( x1 in X & x2 in X implies dist (x1,x2) <= 1 )
assume that
A3: x1 in X and
A4: x2 in X ; :: thesis: dist (x1,x2) <= 1
A5: x2 = x by A4, TARSKI:def 1;
x1 = x by A3, TARSKI:def 1;
hence dist (x1,x2) <= 1 by A5, METRIC_1:1; :: thesis: verum
end;
A6: now :: thesis: for i being Nat holds S . i is bounded
let i be Nat; :: thesis: S . i is bounded
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
S . i9 = X by FUNCOP_1:7;
hence S . i is bounded by A2; :: thesis: verum
end;
for x being object st x in dom S holds
not S . x is empty by FUNCOP_1:7;
hence ( S is pointwise_bounded & S is non-empty ) by A6, FUNCT_1:def 9; :: thesis: verum