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 -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )
let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) )
assume A1: the carrier of L in W ; :: thesis: ( L is Object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )

hereby :: thesis: ( L is strict & L is complete & L is algebraic implies L is Object of (W -ALG_category) )

assume L is Object of (W -ALG_category) ; :: thesis: ( L is strict & L is complete & L is algebraic )
then reconsider a = L as Object of (W -ALG_category) ;
( L = latt a & a is Object of (W -CONT_category) ) by ALTCAT_2:29;
hence ( L is strict & L is complete & L is algebraic ) by A1, Def12, Th16; :: thesis: verum

end;

assume A2: ( L is strict & L is complete & L is algebraic ) ; :: thesis: L is Object of (W -ALG_category)
then reconsider a = L as Object of (W -CONT_category) by A1, Th16;
latt a = L ;
hence L is Object of (W -ALG_category) by A2, Def12; :: thesis: verum