theorem Th30: :: MEASUR12:30

for A being Subset of REAL holds
( Svc2 A c= Svc A & inf (Svc A) <= inf (Svc2 A) )