let S, T be non empty Poset; for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let g be Function of S,T; for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let d be Function of T,S; ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
assume that
A5:
d is monotone
and
A6:
for s being Element of S holds g . s is_maximum_of d " (downarrow s)
; [g,d] is Galois
A7:
for t being Element of T
for s being Element of S holds
( s >= d . t iff g . s >= t )
g is monotone
hence
[g,d] is Galois
by A5, A7; verum