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 Th16, SUBSET_1:63;
hence P is bounded by A1, Th19, Th21; :: thesis: verum