set
C
= the
constant
Loop
of
a
;
set
E
=
EqRel
(
T
,
a
);
the
carrier
of
(
pi_1
(
T
,
a
)
)
=
Class
(
EqRel
(
T
,
a
)
)
by
TOPALG_1:def 5
;
then
{
(
Class
(
(
EqRel
(
T
,
a
)
)
, the
constant
Loop
of
a
)
)
}
=
Class
(
EqRel
(
T
,
a
)
)
by
Th3
;
hence
pi_1
(
T
,
a
) is
trivial
by
TOPALG_1:def 5
;
:: thesis:
verum