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

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