let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )
let d be Function of T,S; :: thesis: ( [g,d] is Galois implies ( g is upper_adjoint & d is lower_adjoint ) )
assume A1: [g,d] is Galois ; :: thesis: ( g is upper_adjoint & d is lower_adjoint )
hence ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def 11 :: thesis: d is lower_adjoint
thus ex g being Function of S,T st [g,d] is Galois by A1; :: according to WAYBEL_1:def 12 :: thesis: verum