theorem Th27: :: WAYBEL25:27

for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is monotone-convergence holds
T is monotone-convergence