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) ) ) )