let FT be non empty RelStr ; :: thesis: for A, C being Subset of FT
for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected

let A, C be Subset of FT; :: thesis: for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected

let D be non empty Subset of FT; :: thesis: ( FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D implies ([#] FT) \ C is connected )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: D = ([#] FT) \ A and
A3: FT is connected and
A4: A is connected and
A5: C is_a_component_of D ; :: thesis: ([#] FT) \ C is connected
consider C1 being Subset of (FT | D) such that
A6: C1 = C and
A7: C1 is_a_component_of FT | D by A5;
reconsider C2 = C1 as Subset of FT by A6;
C1 c= [#] (FT | D) ;
then C1 c= ([#] FT) \ A by ;
then A8: (([#] FT) \ A) ` c= C2 ` by SUBSET_1:12;
then A9: A c= C2 ` by PRE_TOPC:3;
A10: A c= ([#] FT) \ C2 by ;
A11: C1 is connected by A7;
now :: thesis: for P, Q being Subset of FT st ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT
A misses C1 by ;
then A12: A /\ C1 = {} ;
let P, Q be Subset of FT; :: thesis: ( ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT )
assume that
A13: ([#] FT) \ C = P \/ Q and
A14: P misses Q and
A15: P,Q are_separated ; :: thesis: ( P = {} FT or Q = {} FT )
A16: C is connected by ;
A17: now :: thesis: ( A c= Q implies P = {} FT )
assume A18: A c= Q ; :: thesis: P = {} FT
P c= Q ` by ;
then ( Q misses Q ` & A /\ P c= Q /\ (Q `) ) by ;
then A19: A /\ P c= {} ;
(C \/ P) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by ;
then C \/ P misses A ;
then C \/ P c= A ` by SUBSET_1:23;
then C \/ P c= [#] (FT | D) by ;
then reconsider C1P1 = C \/ P as Subset of (FT | D) ;
C \/ P is connected by A1, A3, A13, A15, A16, Th36;
then A20: C1P1 is connected by Th37;
C c= C1 \/ P by ;
then C1P1 = C1 by A6, A7, A20;
then A21: P c= C by ;
P c= ([#] FT) \ C by ;
then ( C misses C ` & P c= C /\ (([#] FT) \ C) ) by ;
then P c= {} ;
hence P = {} FT by XBOOLE_1:3; :: thesis: verum
end;
A22: P misses P ` by XBOOLE_1:79;
A23: Q c= ([#] FT) \ C by ;
now :: thesis: ( A c= P implies Q = {} FT )
assume A24: A c= P ; :: thesis: Q = {} FT
Q c= P ` by ;
then A /\ Q c= P /\ (P `) by ;
then A25: A /\ Q c= {} by A22;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by ;
then C \/ Q misses A ;
then C \/ Q c= A ` by SUBSET_1:23;
then C \/ Q c= [#] (FT | D) by ;
then reconsider C1Q1 = C \/ Q as Subset of (FT | D) ;
C \/ Q is connected by A1, A3, A13, A15, A16, Th36;
then A26: C1Q1 is connected by Th37;
C1 c= C1 \/ Q by XBOOLE_1:7;
then C1Q1 = C1 by A6, A7, A26;
then Q c= C by ;
then ( C misses C ` & Q c= C /\ (([#] FT) \ C) ) by ;
then Q c= {} ;
hence Q = {} FT by XBOOLE_1:3; :: thesis: verum
end;
hence ( P = {} FT or Q = {} FT ) by A1, A4, A6, A10, A13, A15, A17, Th32; :: thesis: verum
end;
hence ([#] FT) \ C is connected by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.72335297,"math_prob":0.9986072,"size":3374,"snap":"2022-40-2023-06","text_gpt3_token_len":1500,"char_repetition_ratio":0.19020772,"word_repetition_ratio":0.31695905,"special_character_ratio":0.5053349,"punctuation_ratio":0.20430107,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99990785,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-09-26T08:26:11Z\",\"WARC-Record-ID\":\"<urn:uuid:e02ad32e-2c09-4791-b8eb-45865d48c12b>\",\"Content-Length\":\"47740\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:d5febbba-0234-4b04-af81-e56eda83960f>\",\"WARC-Concurrent-To\":\"<urn:uuid:ae85c120-9663-428c-908b-183bdabfcc93>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/fintopo6/52\",\"WARC-Payload-Digest\":\"sha1:2FU37YLLHBHPGUEKW6SLDWDHVDGINIYB\",\"WARC-Block-Digest\":\"sha1:27U2OV7CKSZGSHHIX7T5DDEN2FX2VDR2\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030334855.91_warc_CC-MAIN-20220926082131-20220926112131-00695.warc.gz\"}"}