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 ) )

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

( 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 A2:
( L is strict & L is complete & L is algebraic )
; :: thesis: 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;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

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