let W be with_non-empty_element set ; :: thesis: for L being LATTICE st the carrier of L in W holds
( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )
let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) )
assume A1: the carrier of L in W ; :: thesis: ( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

hereby :: thesis: ( L is strict & L is complete & L is continuous implies L is Object of (W -CONT_category) )

assume L is Object of (W -CONT_category) ; :: thesis: ( L is strict & L is complete & L is continuous )
then reconsider a = L as Object of (W -CONT_category) ;
( L = latt a & a is Object of (W -UPS_category) ) by ALTCAT_2:29;
hence ( L is strict & L is complete & L is continuous ) by A1, Def11, Th14; :: thesis: verum

end;

assume A2: ( L is strict & L is complete & L is continuous ) ; :: thesis: L is Object of (W -CONT_category)
then reconsider a = L as Object of (W -UPS_category) by A1, Th14;
latt a = L ;
hence L is Object of (W -CONT_category) by A2, Def11; :: thesis: verum