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:
d is V13() by ;
then A3: the carrier of () |` d is one-to-one by FUNCT_1:58;
A4: d is monotone by ;
A5: now :: thesis: for x, y being Element of T holds
( ( x <= y implies () . x <= () . y ) & ( () . x <= () . y implies x <= y ) )
let x, y be Element of T; :: thesis: ( ( x <= y implies () . x <= () . y ) & ( () . x <= () . y implies x <= y ) )
thus ( x <= y implies () . x <= () . y ) by ; :: thesis: ( () . x <= () . y implies x <= y )
thus ( (corestr d) . x <= () . y implies x <= y ) :: thesis: verum
proof
for t being Element of T holds d . t is_minimum_of g " {t} by ;
then A6: g * d = id T by WAYBEL_1:23;
assume A7: (corestr d) . x <= () . 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 ;
( d . x = () . x & d . y = () . y ) by WAYBEL_1:30;
then d . x <= d . y by ;
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 ;
then (g * d) . x <= (g * d) . y by ;
then (id T) . x <= y by A6;
hence x <= y ; :: thesis: verum
end;
end;
rng () = the carrier of () by FUNCT_2:def 3;
then corestr d is isomorphic by ;
hence T, Image d are_isomorphic ; :: thesis: verum