4.6.4 Dividing Sentences With Assume

For the difference in writing a method after such that, a similar thing occurs in the case of assume. For example, adding & S[x,y] to an assume example, we will assume that the following occurred.

for x,y st P[x,y] & S[x,y] holds Q[x,y]
proof
let x,y;
assume P[x,y] & S[x,y];
······
······
thus Q[x,y];
end;

At this point,

assume P[x,y] & S[x,y];

can be written as below.

assume that L1:P[x,y] and L2:S[x,y];

Only with the way of writing the above formula, we can write labels on both P[x,y] and S[x,y]. In this example, they are L1 and L2 labels.
{"ft_lang_label":"__label__en","ft_lang_prob":0.8684817,"math_prob":0.98941,"size":584,"snap":"2021-31-2021-39","text_gpt3_token_len":180,"char_repetition_ratio":0.17413794,"word_repetition_ratio":0.0,"special_character_ratio":0.3219178,"punctuation_ratio":0.21686748,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9999881,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-07-30T01:40:47Z\",\"WARC-Record-ID\":\"<urn:uuid:11aff6a2-8970-4865-b30f-8158c3264ca0>\",\"Content-Length\":\"2473\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:aef27410-7247-477f-9a46-aa8863ae2721>\",\"WARC-Concurrent-To\":\"<urn:uuid:e53778e7-7311-413e-bdac-f7ff8044076b>\",\"WARC-IP-Address\":\"160.252.134.18\",\"WARC-Target-URI\":\"http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/en_wframe/chapter4_6_4.html\",\"WARC-Payload-Digest\":\"sha1:EFJCU5ICEMPAQSKPXR5ZFWYNYWZNOBU5\",\"WARC-Block-Digest\":\"sha1:OWWSQY3O2QEVE5642Q4RQDK6X3VQBLOV\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-31/CC-MAIN-2021-31_segments_1627046153899.14_warc_CC-MAIN-20210729234313-20210730024313-00467.warc.gz\"}"}