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 onto & [g,d] is Galois holds
T, Image d are_isomorphic
let g be Function of S,T; :: thesis: for d being Function of T,S st g is onto & [g,d] is Galois holds
T, Image d are_isomorphic
let d be Function of T,S; :: thesis: ( g is onto & [g,d] is Galois implies T, Image d are_isomorphic )
assume that
A1: g is onto and
A2: [g,d] is Galois ; :: thesis: T, Image d are_isomorphic
d is one-to-one by A1, A2, WAYBEL_1:26;
then A3: the carrier of (Image d) | d is one-to-one by FUNCT_1:99;
A4: rng (corestr d) = the carrier of (Image d) by FUNCT_2:def 3;
B5: d is monotone by A2, WAYBEL_1:9;

now

let x, y be Element of T; :: thesis: ( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )
thus ( x <= y implies (corestr d) . x <= (corestr d) . y ) by B5, WAYBEL_1:def 2; :: thesis: ( (corestr d) . x <= (corestr d) . y implies x <= y )
thus ( (corestr d) . x <= (corestr d) . y implies x <= y ) :: thesis: verum

proof

A6: ( d . x = (corestr d) . x & d . y = (corestr d) . y ) by WAYBEL_1:32;
A7: g is monotone by A2, WAYBEL_1:9;
for t being Element of T holds d . t is_minimum_of g " {t} by A1, A2, WAYBEL_1:23;
then A8: g * d = id T by WAYBEL_1:24;
x in the carrier of T ;
then A9: x in dom d by FUNCT_2:def 1;
y in the carrier of T ;
then A10: y in dom d by FUNCT_2:def 1;
assume (corestr d) . x <= (corestr d) . y ; :: thesis: x <= y
then d . x <= d . y by A6, YELLOW_0:60;
then g . (d . x) <= g . (d . y) by A7, WAYBEL_1:def 2;
then (g * d) . x <= g . (d . y) by A9, FUNCT_1:23;
then (g * d) . x <= (g * d) . y by A10, FUNCT_1:23;
then (id T) . x <= y by A8, FUNCT_1:35;
hence x <= y by FUNCT_1:35; :: thesis: verum

end;

end;

then corestr d is isomorphic by A3, A4, WAYBEL_0:66;
hence T, Image d are_isomorphic by WAYBEL_1:def 8; :: thesis: verum