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