a is LATTICE by Def4;
hence for b₁ being LATTICE holds
( b₁ = a as_1-sorted iff b₁ = a ) by Def1; :: thesis: verum