let S, T be non empty Poset; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: [g,d] is Galois
for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )

proof

let t be Element of T; :: thesis: for s being Element of S holds
( t <= g . s iff d . t <= s )
let s be Element of S; :: thesis: ( t <= g . s iff d . t <= s )

hereby :: thesis: ( d . t <= s implies t <= g . s )

(d * g) . s <= (id S) . s by A3, YELLOW_2:9;
then d . (g . s) <= (id S) . s by FUNCT_2:15;
then A5: d . (g . s) <= s ;
assume t <= g . s ; :: thesis: d . t <= s
then d . t <= d . (g . s) by A2;
hence d . t <= s by A5, ORDERS_2:3; :: thesis: verum

end;

(id T) . t <= (g * d) . t by A4, YELLOW_2:9;
then (id T) . t <= g . (d . t) by FUNCT_2:15;
then A6: t <= g . (d . t) ;
assume d . t <= s ; :: thesis: t <= g . s
then g . (d . t) <= g . s by A1;
hence t <= g . s by A6, ORDERS_2:3; :: thesis: verum

end;

hence [g,d] is Galois by A1, A2; :: thesis: verum