theorem Th3: :: OSALG_2:3

for S0 being non empty non void strict all-with_const_op ManySortedSign holds OSSign S0 is all-with_const_op