begin
begin
begin
Lm1:
for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
begin
begin
deffunc H1( set ) -> set = $1;