let T be non empty TopStruct ; 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; 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; ( 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 )
; 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 )
; 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; verum