let W be with_non-empty_element set ; :: thesis: for x being set holds
( x is object of (W -UPS_category ) iff ( x is complete LATTICE & x in POSETS W ) )
let x be set ; :: thesis: ( x is object of (W -UPS_category ) iff ( x is complete LATTICE & x in POSETS W ) )

hereby :: thesis: ( x is complete LATTICE & x in POSETS W implies x is object of (W -UPS_category ) )

assume x is object of (W -UPS_category ) ; :: thesis: ( x is complete LATTICE & x in POSETS W )
then reconsider a = x as object of (W -UPS_category ) ;
latt a = x ;
hence x is complete LATTICE ; :: thesis: x in POSETS W
( a in the carrier of (W -UPS_category ) & the carrier of (W -UPS_category ) c= POSETS W ) by Th12;
hence x in POSETS W ; :: thesis: verum

end;

assume x is complete LATTICE ; :: thesis: ( not x in POSETS W or x is object of (W -UPS_category ) )
then reconsider L = x as complete LATTICE ;
assume x in POSETS W ; :: thesis: x is object of (W -UPS_category )
then ( L as_1-sorted = L & the carrier of (L as_1-sorted ) in W & L is strict ) by Def1, Def2;
hence x is object of (W -UPS_category ) by Def10; :: thesis: verum