theorem Th21: :: WAYBEL28:21

for L being non empty 1-sorted
for C1, C2 being Convergence-Class of L st C1 c= C2 holds
the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)