let W be with_non-empty_element set ; :: thesis: for L being LATTICE holds
( L is Object of (W -INF_category) iff ( L is strict & L is complete & the carrier of L in W ) )
ex a being non empty set st a in W by SETFAM_1:def 10;
hence for L being LATTICE holds
( L is Object of (W -INF_category) iff ( L is strict & L is complete & the carrier of L in W ) ) by Def4; :: thesis: verum