theorem Th12:
for
T being non
empty TopSpace holds
(
T is
simply_connected iff for
t1,
t2 being
Point of
T holds
(
t1,
t2 are_connected & ( for
P,
Q being
Path of
t1,
t2 holds
Class (
(EqRel (T,t1,t2)),
P)
= Class (
(EqRel (T,t1,t2)),
Q) ) ) )