let T be non empty TopStruct ; :: thesis: for Q1, Q2 being Subset of T
for p1, p2 being Point of T st Q1 /\ Q2 = {} & Q1 \/ Q2 = the carrier of T & p1 in Q1 & p2 in Q2 & Q1 is open & Q2 is open holds
for P being Function of I[01],T holds
( not P is continuous or not P . 0 = p1 or not P . 1 = p2 )
let Q1, Q2 be Subset of T; :: thesis: for p1, p2 being Point of T st Q1 /\ Q2 = {} & Q1 \/ Q2 = the carrier of T & p1 in Q1 & p2 in Q2 & Q1 is open & Q2 is open holds
for P being Function of I[01],T holds
( not P is continuous or not P . 0 = p1 or not P . 1 = p2 )
let p1, p2 be Point of T; :: thesis: ( Q1 /\ Q2 = {} & Q1 \/ Q2 = the carrier of T & p1 in Q1 & p2 in Q2 & Q1 is open & Q2 is open implies for P being Function of I[01],T holds
( not P is continuous or not P . 0 = p1 or not P . 1 = p2 ) )
assume that
A1: Q1 /\ Q2 = {} and
A2: Q1 \/ Q2 = the carrier of T and
A3: p1 in Q1 and
A4: p2 in Q2 and
A5: ( Q1 is open & Q2 is open ) ; :: thesis: for P being Function of I[01],T holds
( not P is continuous or not P . 0 = p1 or not P . 1 = p2 )
assume ex P being Function of I[01],T st
( P is continuous & P . 0 = p1 & P . 1 = p2 ) ; :: thesis: contradiction
then consider P being Function of I[01],T such that
A6: P is continuous and
A7: P . 0 = p1 and
A8: P . 1 = p2 ;
[#] T <> {} ;
then A9: ( P " Q1 is open & P " Q2 is open ) by A5, A6, TOPS_2:43;
A10: [#] I[01] = [.0,1.] by TOPMETR:18, TOPMETR:20;
then 0 in the carrier of I[01] by XXREAL_1:1;
then 0 in dom P by FUNCT_2:def 1;
then A11: ( [#] I[01] = the carrier of I[01] & P " Q1 <> {} I[01] ) by A3, A7, FUNCT_1:def 7;
(P " Q1) /\ (P " Q2) = P " (Q1 /\ Q2) by FUNCT_1:68
.= {} by A1 ;
then A12: not P " Q1 meets P " Q2 by XBOOLE_0:def 7;
1 in the carrier of I[01] by A10, XXREAL_1:1;
then 1 in dom P by FUNCT_2:def 1;
then A13: P " Q2 <> {} I[01] by A4, A8, FUNCT_1:def 7;
(P " Q1) \/ (P " Q2) = P " (Q1 \/ Q2) by RELAT_1:140
.= the carrier of I[01] by A2, FUNCT_2:40 ;
hence contradiction by A9, A11, A13, A12, CONNSP_1:11, TREAL_1:19; :: thesis: verum