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 ) )
A1: [#] T <> {} ;
assume A2: ( Q1 /\ Q2 = {} & Q1 \/ Q2 = the carrier of T & p1 in Q1 & p2 in Q2 & 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
A3: ( P is continuous & P . 0 = p1 & P . 1 = p2 ) ;
A4: P " Q1 is open by A1, A2, A3, TOPS_2:55;
A5: P " Q2 is open by A1, A2, A3, TOPS_2:55;
A6: [#] I[01] = the carrier of I[01] ;
A7: [#] I[01] = [.0 ,1.] by TOPMETR:25, TOPMETR:27;
then 0 in the carrier of I[01] by XXREAL_1:1;
then 0 in dom P by FUNCT_2:def 1;
then A8: P " Q1 <> {} I[01] by A2, A3, FUNCT_1:def 13;
1 in the carrier of I[01] by A7, XXREAL_1:1;
then 1 in dom P by FUNCT_2:def 1;
then A9: P " Q2 <> {} I[01] by A2, A3, FUNCT_1:def 13;
A10: (P " Q1) \/ (P " Q2) = P " (Q1 \/ Q2) by RELAT_1:175
.= the carrier of I[01] by A2, FUNCT_2:48 ;
(P " Q1) /\ (P " Q2) = P " (Q1 /\ Q2) by FUNCT_1:137
.= {} by A2, RELAT_1:171 ;
then not P " Q1 meets P " Q2 by XBOOLE_0:def 7;
hence contradiction by A4, A5, A6, A8, A9, A10, CONNSP_1:12, TREAL_1:22; :: thesis: verum