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 -UPS_category) iff ( L is strict & L is complete ) )
let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) ) )
assume A1: the carrier of L in W ; :: thesis: ( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) )
L as_1-sorted = L by Def1;
then ( L in POSETS W iff L is strict ) by A1, Def2;
hence ( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) ) by Th13; :: thesis: verum