let GX be TopSpace; :: thesis: for A, C being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds
C meets Fr A
let A, C 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:18;
Cl (C /\ A) c= Cl A by PRE_TOPC:19, 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:18;
A7: C \ A = C /\ (A `) by SUBSET_1:13;
then Cl (C \ A) c= Cl (A `) by PRE_TOPC:19, 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:2
.= (C /\ A) \/ (C \ A) by A7, XBOOLE_1:23 ;
C /\ A <> {} by A2;
then not C /\ A,C \ A are_separated by A1, A3, A9, Th15;
then ( Cl (C /\ A) meets C \ A or C /\ A meets Cl (C \ A) ) ;
then A10: ( (Cl (C /\ A)) /\ (C \ A) <> {} or (C /\ A) /\ (Cl (C \ A)) <> {} ) ;
((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