a
,
b
are_connected
by
Def3
;
hence
for
b
_{1}
being
Function
of
I[01]
,
T
holds
(
b
_{1}
is
Path
of
a
,
b
iff (
b
_{1}
is
continuous
&
b
_{1}
.
0
=
a
&
b
_{1}
.
1
=
b
) )
by
Def2
;
:: thesis:
verum