Theorem UpperSet.prod_self_lt_prod_self

Modification history