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 . () = sup () by YELLOW_2:def 3
.= y9 by WAYBEL_0:34 ;
hence y in rng g by ; :: 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:
thus g is infs-preserving by ; :: thesis:
g is sups-preserving by ;
hence g is directed-sups-preserving ; :: thesis: verum