a "/\" is lower_adjoint by A1, Def19;
hence ex b₁ being Function of H,H st [b₁,(a "/\")] is Galois by Def12; :: thesis: verum