set g = the infs-preserving Function of S,T;
the infs-preserving Function of S,T is upper_adjoint by WAYBEL_1:16;
then ex d being Function of T,S st [ the infs-preserving Function of S,T,d] is Galois ;
hence ex b₁ being Connection of S,T st b₁ is Galois ; :: thesis: verum