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

hence S is complete LATTICE ; :: thesis: verum

( 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

then
S is non empty complete Poset
by YELLOW_2:28;
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;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

hence S is complete LATTICE ; :: thesis: verum