let S, T be non empty Poset; for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois
let g be Function of S,T; for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois
let d be Function of T,S; ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies [g,d] is Galois )
assume that
A1:
g is monotone
and
A2:
d is monotone
and
A3:
d * g <= id S
and
A4:
id T <= g * d
; [g,d] is Galois
for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )
hence
[g,d] is Galois
by A1, A2; verum