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
( g is onto iff d is one-to-one )
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is one-to-one )
let d be Function of T,S; :: thesis: ( [g,d] is Galois implies ( g is onto iff d is one-to-one ) )
assume A1: [g,d] is Galois ; :: thesis: ( g is onto iff d is one-to-one )

hereby :: thesis: ( d is one-to-one implies g is onto )

assume g is onto ; :: thesis: d is one-to-one
then for t being Element of T holds d . t is_minimum_of g " {t} by A1, Th23;
then g * d = id T by Th24;
hence d is one-to-one by Th25; :: thesis: verum

end;

assume A2: d is one-to-one ; :: thesis: g is onto
A3: ( the carrier of T = dom d & the carrier of T = dom (g * d) & rng (g * d) c= the carrier of T ) by FUNCT_2:def 1;
A4: ( g is monotone & d is monotone ) by A1, Th9;
( d * g <= id S & id T <= g * d ) by A1, Th19;
then d = (d * g) * d by A4, Th21
.= d * (g * d) by RELAT_1:55 ;
then g * d = id T by A2, A3, FUNCT_1:50;
hence g is onto by Th25; :: thesis: verum