consider g being infs-preserving Function of S,T;
g is upper_adjoint by WAYBEL_1:17;
then ex d being Function of T,S st [g,d] is Galois by WAYBEL_1:def 11;
hence ex b₁ being Connection of S,T st b₁ is Galois ; :: thesis: verum