a is LATTICE by Def4;
hence a as_1-sorted is LATTICE by Def1; :: thesis: verum