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

( 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