let W be with_non-empty_element set ; :: thesis: the carrier of (W -UPS_category) c= POSETS W

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W -UPS_category) or x in POSETS W )

assume x in the carrier of (W -UPS_category) ; :: thesis: x in POSETS W

then reconsider x = x as Object of (W -UPS_category) ;

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

then A2: the carrier of (latt x) in W by Def10;

latt x = x ;

then x is strict Poset by A1, Def10;

hence x in POSETS W by A2, Def2; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W -UPS_category) or x in POSETS W )

assume x in the carrier of (W -UPS_category) ; :: thesis: x in POSETS W

then reconsider x = x as Object of (W -UPS_category) ;

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

then A2: the carrier of (latt x) in W by Def10;

latt x = x ;

then x is strict Poset by A1, Def10;

hence x in POSETS W by A2, Def2; :: thesis: verum