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 ;
hence P is bounded by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.8979738,"math_prob":0.9873013,"size":403,"snap":"2019-43-2019-47","text_gpt3_token_len":143,"char_repetition_ratio":0.18796992,"word_repetition_ratio":0.25287357,"special_character_ratio":0.34739456,"punctuation_ratio":0.114583336,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9999217,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-16T08:14:45Z\",\"WARC-Record-ID\":\"<urn:uuid:f557a30b-cd70-40ad-a2fa-3474767dbaa5>\",\"Content-Length\":\"5694\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:fac5f83c-349f-4a61-b768-1ceee8e20d7b>\",\"WARC-Concurrent-To\":\"<urn:uuid:666bf2b6-632d-4ccc-aec5-fab2ca927dac>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"http://mizar.uwb.edu.pl/version/current/html/proofs/tbsp_1/29\",\"WARC-Payload-Digest\":\"sha1:6GWPPGNJTPGHL7E64BEQPCNDRDTTMOLF\",\"WARC-Block-Digest\":\"sha1:X5KDHRIQIJCD6DORNBH2DWYGF47TBZD2\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986666467.20_warc_CC-MAIN-20191016063833-20191016091333-00211.warc.gz\"}"}