:: deftheorem defines simply_connected TOPALG_6:def 2 :
for T being non empty TopSpace holds
( T is simply_connected iff ( T is having_trivial_Fundamental_Group & T is pathwise_connected ) );