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 V13() )
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 V13() )
let d be Function of T,S; :: thesis: ( [g,d] is Galois implies ( g is onto iff d is V13() ) )
A1: ( the carrier of T = dom d & the carrier of T = dom (g * d) ) by FUNCT_2:def 1;
assume A2: [g,d] is Galois ; :: thesis: ( g is onto iff d is V13() )
then A3: ( d * g <= id S & id T <= g * d ) by Th18;
hereby :: thesis: ( d is V13() implies g is onto )
assume g is onto ; :: thesis: d is V13()
then for t being Element of T holds d . t is_minimum_of g " {t} by A2, Th22;
then g * d = id T by Th23;
hence d is V13() by FUNCT_2:23; :: thesis: verum
end;
A4: rng (g * d) c= the carrier of T ;
( g is monotone & d is monotone ) by A2, Th8;
then A5: d = (d * g) * d by A3, Th20
.= d * (g * d) by RELAT_1:36 ;
assume d is V13() ; :: thesis: g is onto
then g * d = id T by A1, A4, A5, FUNCT_1:28;
hence g is onto by FUNCT_2:23; :: thesis: verum