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