let L be lower-bounded LATTICE; :: thesis: ( L is continuous implies ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
assume A1: L is continuous ; :: thesis: ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
reconsider A = InclPoset (Ids L) as lower-bounded arithmetic LATTICE by WAYBEL13:14;
take A ; :: thesis: ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
reconsider g = SupMap L as Function of A,L ;
take g ; :: thesis: ( g is onto & g is infs-preserving & g is directed-sups-preserving )
the carrier of L c= rng g

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of L or y in rng g )
assume y in the carrier of L ; :: thesis: y in rng g
then reconsider y9 = y as Element of L ;
downarrow y9 is Element of A by YELLOW_2:41;
then downarrow y9 in the carrier of A ;
then A2: downarrow y9 in dom g by FUNCT_2:def 1;
g . (downarrow y9) = sup (downarrow y9) by YELLOW_2:def 3
.= y9 by WAYBEL_0:34 ;
hence y in rng g by A2, FUNCT_1:def 3; :: thesis: verum

end;

then rng g = the carrier of L by XBOOLE_0:def 10;
hence g is onto by FUNCT_2:def 3; :: thesis: ( g is infs-preserving & g is directed-sups-preserving )
thus g is infs-preserving by A1, WAYBEL13:33; :: thesis: g is directed-sups-preserving
g is sups-preserving by A1, WAYBEL13:33;
hence g is directed-sups-preserving ; :: thesis: verum