for L being trivial Semilattice holds L is modular by STRUCT_0:def 10;