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