let L be complete LATTICE; :: thesis: for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is onto ) holds
S is complete LATTICE
let S be non empty Poset; :: thesis: ( ex g being Function of L,S st
( g is infs-preserving & g is onto ) implies S is complete LATTICE )
given g being Function of L,S such that A1: g is infs-preserving and
A2: g is onto ; :: thesis: S is complete LATTICE
for A being Subset of S holds ex_inf_of A,S

proof

let A be Subset of S; :: thesis: ex_inf_of A,S
set Y = g " A;
rng g = the carrier of S by A2, FUNCT_2:def 3;
then A3: A = g .: (g " A) by FUNCT_1:77;
( ex_inf_of g " A,L & g preserves_inf_of g " A ) by A1, WAYBEL_0:def 32, YELLOW_0:17;
hence ex_inf_of A,S by A3, WAYBEL_0:def 30; :: thesis: verum

end;

then S is non empty complete Poset by YELLOW_2:28;
hence S is complete LATTICE ; :: thesis: verum