let W be with_non-empty_element set ; :: thesis: for L being LATTICE holds
( L is object of (W -INF(SC)_category ) iff ( L is strict & L is complete & the carrier of L in W ) )
let L be LATTICE; :: thesis: ( L is object of (W -INF(SC)_category ) iff ( L is strict & L is complete & the carrier of L in W ) )
the carrier of (W -INF(SC)_category ) c= the carrier of (W -INF_category ) by ALTCAT_2:def 11;
then ( L in the carrier of (W -INF(SC)_category ) implies L is object of (W -INF_category ) ) ;
then ( L is object of (W -INF(SC)_category ) iff L is object of (W -INF_category ) ) by Def10;
hence ( L is object of (W -INF(SC)_category ) iff ( L is strict & L is complete & the carrier of L in W ) ) by Th13; :: thesis: verum