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:30;
hence ( L is strict & L is complete & L is algebraic ) by A1, Def12, Th17; :: 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, Th17;
latt a = L ;
hence L is object of (W -ALG_category ) by A2, Def12; :: thesis: verum