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 and
A3: C \ A <> {} GX ; :: thesis: C meets Fr A
A4: A ` c= Cl (A ` ) by PRE_TOPC:48;
Cl (C /\ A) c= Cl A by PRE_TOPC:49, XBOOLE_1:17;
then A5: (Cl (C /\ A)) /\ (A ` ) c= (Cl A) /\ (Cl (A ` )) by A4, XBOOLE_1:27;
A6: A c= Cl A by PRE_TOPC:48;
A7: C \ A = C /\ (A ` ) by SUBSET_1:32;
then Cl (C \ A) c= Cl (A ` ) by PRE_TOPC:49, XBOOLE_1:17;
then A /\ (Cl (C /\ (A ` ))) c= (Cl A) /\ (Cl (A ` )) by A7, A6, XBOOLE_1:27;
then ((Cl (C /\ A)) /\ (A ` )) \/ (A /\ (Cl (C /\ (A ` )))) c= (Cl A) /\ (Cl (A ` )) by A5, XBOOLE_1:8;
then A8: C /\ (((Cl (C /\ A)) /\ (A ` )) \/ (A /\ (Cl (C /\ (A ` ))))) c= C /\ ((Cl A) /\ (Cl (A ` ))) by XBOOLE_1:27;
A9: C = C /\ ([#] GX) by XBOOLE_1:28
.= C /\ (A \/ (A ` )) by PRE_TOPC:18
.= (C /\ A) \/ (C \ A) by A7, XBOOLE_1:23 ;
C /\ A <> {} by A2, XBOOLE_0:def 7;
then not C /\ A,C \ A are_separated by A1, A3, A9, 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;
((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) = (((Cl (C /\ A)) /\ C) /\ (A ` )) \/ ((C /\ A) /\ (Cl (C /\ (A ` )))) by A7, 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 ;
then ((Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ (Cl (C \ A))) c= C /\ (Fr A) by A8, TOPS_1:def 2;
hence C /\ (Fr A) <> {} by A10; :: according to XBOOLE_0:def 7 :: thesis: verum