let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for t1 being Element of T
for P being Subset of T st P = {t1} holds
P is bounded
let t1 be Element of T; :: thesis: for P being Subset of T st P = {t1} holds
P is bounded
let P be Subset of T; :: thesis: ( P = {t1} implies P is bounded )
assume A1: P = {t1} ; :: thesis: P is bounded
{t1} is Subset of (Ball (t1,1)) by Th11, SUBSET_1:41;
hence P is bounded by A1, Th14; :: thesis: verum