let L be RelStr ; :: thesis: for S being Subset of L holds
( id S is Function of (),L & ( for f being Function of (),L st f = id S holds
f is monotone ) )

let S be Subset of L; :: thesis: ( id S is Function of (),L & ( for f being Function of (),L st f = id S holds
f is monotone ) )

A1: the carrier of () = S by YELLOW_0:def 15;
A2: rng (id S) = S by RELAT_1:45;
dom (id S) = S by RELAT_1:45;
hence id S is Function of (),L by ; :: thesis: for f being Function of (),L st f = id S holds
f is monotone

let f be Function of (),L; :: thesis: ( f = id S implies f is monotone )
assume A3: f = id S ; :: thesis: f is monotone
let x, y be Element of (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )

assume A4: [x,y] in the InternalRel of () ; :: according to ORDERS_2:def 5 :: thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )

let a, b be Element of L; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume that
A5: a = f . x and
A6: b = f . y ; :: thesis: a <= b
x in S by ;
then A7: a = x by ;
y in S by ;
then A8: b = y by ;
the InternalRel of () c= the InternalRel of L by YELLOW_0:def 13;
hence [a,b] in the InternalRel of L by A4, A7, A8; :: according to ORDERS_2:def 5 :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.72813684,"math_prob":0.9990833,"size":1423,"snap":"2022-40-2023-06","text_gpt3_token_len":574,"char_repetition_ratio":0.16208598,"word_repetition_ratio":0.39534885,"special_character_ratio":0.40337315,"punctuation_ratio":0.18441558,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9998079,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-10-03T21:31:24Z\",\"WARC-Record-ID\":\"<urn:uuid:07d53c31-67e1-4cb8-939d-778e7627682c>\",\"Content-Length\":\"18187\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:78e20793-3766-4b69-9503-1431f3dfd028>\",\"WARC-Concurrent-To\":\"<urn:uuid:4a615121-9504-4ab5-b6ec-12e83db0c0fb>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/waybel10/14\",\"WARC-Payload-Digest\":\"sha1:3NZADGVX6GFQE6UOJY7H7GZKV3J5VXKC\",\"WARC-Block-Digest\":\"sha1:N4MEKVNCIAW73BLVE2EPKQRCKMGXMCKZ\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030337432.78_warc_CC-MAIN-20221003200326-20221003230326-00341.warc.gz\"}"}