let W be with_non-empty_element set ; :: thesis: the carrier of (W -UPS_category ) c= POSETS W
A1: ex w being non empty set st w in W by SETFAM_1:def 11;
let x be set ; :: 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 ) ;
latt x = x ;
then ( the carrier of (latt x) in W & x is strict Poset ) by A1, Def10;
hence x in POSETS W by Def2; :: thesis: verum