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:24;
then A3: the carrier of (Image d) |` d is one-to-one by FUNCT_1:58;
A4: d is monotone by A2, WAYBEL_1:8;

A5: now :: thesis: for x, y being Element of T holds
( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )

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 A4, 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

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

end;

end;

rng (corestr d) = the carrier of (Image d) by FUNCT_2:def 3;
then corestr d is isomorphic by A3, A5, WAYBEL_0:66;
hence T, Image d are_isomorphic ; :: thesis: verum