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
( d = (d * g) * d & g = (g * d) * g )
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
( d = (d * g) * d & g = (g * d) * g )
let d be Function of T,S; :: thesis: ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies ( d = (d * g) * d & g = (g * d) * g ) )
assume that
A1: g is monotone and
A2: d is monotone and
A3: d * g <= id S and
A4: id T <= g * d ; :: thesis: ( d = (d * g) * d & g = (g * d) * g )
for t being Element of T holds d . t = ((d * g) * d) . t

proof

let t be Element of T; :: thesis: d . t = ((d * g) * d) . t
(id T) . t <= (g * d) . t by A4, YELLOW_2:9;
then t <= (g * d) . t ;
then d . t <= d . ((g * d) . t) by A2;
then d . t <= (d * (g * d)) . t by FUNCT_2:15;
then A5: d . t <= ((d * g) * d) . t by RELAT_1:36;
(d * g) . (d . t) <= (id S) . (d . t) by A3, YELLOW_2:9;
then (d * g) . (d . t) <= d . t ;
then d . t >= ((d * g) * d) . t by FUNCT_2:15;
hence d . t = ((d * g) * d) . t by A5, ORDERS_2:2; :: thesis: verum

end;

hence d = (d * g) * d by FUNCT_2:63; :: thesis: g = (g * d) * g
for s being Element of S holds g . s = ((g * d) * g) . s

proof

let s be Element of S; :: thesis: g . s = ((g * d) * g) . s
(d * g) . s <= (id S) . s by A3, YELLOW_2:9;
then (d * g) . s <= s ;
then g . ((d * g) . s) <= g . s by A1;
then (g * (d * g)) . s <= g . s by FUNCT_2:15;
then A6: g . s >= ((g * d) * g) . s by RELAT_1:36;
(id T) . (g . s) <= (g * d) . (g . s) by A4, YELLOW_2:9;
then g . s <= (g * d) . (g . s) ;
then g . s <= ((g * d) * g) . s by FUNCT_2:15;
hence g . s = ((g * d) * g) . s by A6, ORDERS_2:2; :: thesis: verum

end;

hence g = (g * d) * g by FUNCT_2:63; :: thesis: verum