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

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