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 g9 being Function of S,T, d9 being Function of T,S such that
A1: [g,d] = [g9,d9] and
A2: ( g9 is monotone & d9 is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g9 . s iff d9 . t <= s ) ) ) ;
( g = g9 & d = d9 ) by A1, XTUPLE_0:1;
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 ) ; :: thesis: verum