let GX be TopSpace; :: thesis: for C, A being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds
C meets Fr A
let C, A be Subset of GX; :: thesis: ( C is connected & C meets A & C \ A <> {} GX implies C meets Fr A )
assume that
A1: C is connected and
A2: ( C meets A & C \ A <> {} GX ) ; :: thesis: C meets Fr A
A3: C /\ A <> {} by A2, XBOOLE_0:def 7;
A4: C \ A = C /\ (A ` ) by SUBSET_1:32;
A5: C = C /\ ([#] GX) by XBOOLE_1:28
.= C /\ (A \/ (A ` )) by PRE_TOPC:18
.= (C /\ A) \/ (C \ A) by A4, XBOOLE_1:23 ;
A6: Cl (C /\ A) c= Cl A by PRE_TOPC:49, XBOOLE_1:17;
A7: A ` c= Cl (A ` ) by PRE_TOPC:48;
A8: A c= Cl A by PRE_TOPC:48;
A9: Cl (C \ A) c= Cl (A ` ) by A4, PRE_TOPC:49, XBOOLE_1:17;
not C /\ A,C \ A are_separated by A1, A2, A3, A5, Th16;
then ( Cl (C /\ A) meets C \ A or C /\ A meets Cl (C \ A) ) by Def1;
then A10: ( (Cl (C /\ A)) /\ (C \ A) <> {} or (C /\ A) /\ (Cl (C \ A)) <> {} ) by XBOOLE_0:def 7;
A11: ((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) = (((Cl (C /\ A)) /\ C) /\ (A ` )) \/ ((C /\ A) /\ (Cl (C /\ (A ` )))) by A4, XBOOLE_1:16
.= ((C /\ (Cl (C /\ A))) /\ (A ` )) \/ (C /\ (A /\ (Cl (C /\ (A ` ))))) by XBOOLE_1:16
.= (C /\ ((Cl (C /\ A)) /\ (A ` ))) \/ (C /\ (A /\ (Cl (C /\ (A ` ))))) by XBOOLE_1:16
.= C /\ (((Cl (C /\ A)) /\ (A ` )) \/ (A /\ (Cl (C /\ (A ` ))))) by XBOOLE_1:23 ;
A12: (Cl (C /\ A)) /\ (A ` ) c= (Cl A) /\ (Cl (A ` )) by A6, A7, XBOOLE_1:27;
A /\ (Cl (C /\ (A ` ))) c= (Cl A) /\ (Cl (A ` )) by A4, A8, A9, XBOOLE_1:27;
then ( ((Cl (C /\ A)) /\ (A ` )) \/ (A /\ (Cl (C /\ (A ` )))) c= (Cl A) /\ (Cl (A ` )) & C c= C ) by A12, XBOOLE_1:8;
then C /\ (((Cl (C /\ A)) /\ (A ` )) \/ (A /\ (Cl (C /\ (A ` ))))) c= C /\ ((Cl A) /\ (Cl (A ` ))) by XBOOLE_1:27;
then ((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) c= C /\ (Fr A) by A11, TOPS_1:def 2;
hence C /\ (Fr A) <> {} by A10; :: according to XBOOLE_0:def 7 :: thesis: verum