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 A1: ( the carrier of (L as_1-sorted) in W & L is strict ) by Def2;
L as_1-sorted = L by Def1;
hence x is Object of (W -UPS_category) by A1, Def10; :: thesis: verum