consider S0 being non empty non void strict all-with_const_op ManySortedSign ;
take OSSign S0 ; :: thesis: ( OSSign S0 is all-with_const_op & OSSign S0 is strict )
thus ( OSSign S0 is all-with_const_op & OSSign S0 is strict ) by Th3; :: thesis: verum