let GX be TopSpace; 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; ( 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
; 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; XBOOLE_0:def 7 verum