let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
let g be Function of S,T; :: thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
let d be Function of T,S; :: thesis: ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )

hereby :: thesis: ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois )

assume [g,d] is Galois ; :: thesis: ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) )
then consider g' being Function of S,T, d' being Function of T,S such that
A1: [g,d] = [g',d'] and
A2: ( g' is monotone & d' is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g' . s iff d' . t <= s ) ) ) by Def10;
( g = g' & d = d' ) by A1, ZFMISC_1:33;
hence ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) by A2; :: thesis: verum

end;

thus ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois ) by Def10; :: thesis: verum