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