let A, B be Subset of GX; :: thesis: ( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open implies A meets B )
assume that
A2: [#] GX = A \/ B and
A3: A <> {} GX and
A4: B <> {} GX and
A5: ( A is open & B is open ) ; :: thesis: A meets B
set v = the Element of B;
set u = the Element of A;
reconsider y = the Element of B as Point of GX by A2, A4, XBOOLE_0:def 3;
reconsider x = the Element of A as Point of GX by A2, A3, XBOOLE_0:def 3;
consider GY being non empty TopSpace such that
A6: GY is connected and
A7: ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) by A1;
consider f being Function of GY,GX such that
A8: f is continuous and
A9: x in rng f and
A10: y in rng f by A7;
f " ([#] GX) = [#] GY by Th41;
then A11: (f " A) \/ (f " B) = [#] GY by A2, RELAT_1:140;
(rng f) /\ B <> {} by A4, A10, XBOOLE_0:def 4;
then rng f meets B by XBOOLE_0:def 7;
then A12: f " B <> {} GY by RELAT_1:138;
(rng f) /\ A <> {} by A3, A9, XBOOLE_0:def 4;
then rng f meets A by XBOOLE_0:def 7;
then A13: f " A <> {} GY by RELAT_1:138;
[#] GX <> {} ;
then ( f " A is open & f " B is open ) by A5, A8, Th43;
then f " A meets f " B by A6, A11, A13, A12, CONNSP_1:11;
then (f " A) /\ (f " B) <> {} by XBOOLE_0:def 7;
then f " (A /\ B) <> {} by FUNCT_1:68;
then rng f meets A /\ B by RELAT_1:138;
then ex u1 being object st
( u1 in rng f & u1 in A /\ B ) by XBOOLE_0:3;
hence A meets B by XBOOLE_0:4; :: thesis: verum