let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )
let d be Function of T,S; :: thesis: ( [g,d] is Galois implies ( d * g <= id S & id T <= g * d ) )
assume A1: [g,d] is Galois ; :: thesis: ( d * g <= id S & id T <= g * d )
for s being Element of S holds (d * g) . s <= (id S) . s
proof
let s be Element of S; :: thesis: (d * g) . s <= (id S) . s
d . (g . s) <= s by A1, Th8;
then (d * g) . s <= s by FUNCT_2:15;
hence (d * g) . s <= (id S) . s ; :: thesis: verum
end;
hence d * g <= id S by YELLOW_2:9; :: thesis: id T <= g * d
for t being Element of T holds (id T) . t <= (g * d) . t
proof
let t be Element of T; :: thesis: (id T) . t <= (g * d) . t
t <= g . (d . t) by A1, Th8;
then t <= (g * d) . t by FUNCT_2:15;
hence (id T) . t <= (g * d) . t ; :: thesis: verum
end;
hence id T <= g * d by YELLOW_2:9; :: thesis: verum