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 ) )

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

( 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 complete LATTICE
; :: thesis: ( not x in POSETS W or 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;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

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