let W be with_non-empty_element set ; :: thesis: the carrier of (W -INF_category ) = the carrier of (W -SUP_category )
A1: ex x being non empty set st x in W by SETFAM_1:def 11;
thus the carrier of (W -INF_category ) c= the carrier of (W -SUP_category ) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (W -SUP_category ) c= the carrier of (W -INF_category )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W -INF_category ) or x in the carrier of (W -SUP_category ) )
assume A2: x in the carrier of (W -INF_category ) ; :: thesis: x in the carrier of (W -SUP_category )
then reconsider x = x as LATTICE by YELLOW21:def 4;
( x is strict & x is complete & the carrier of x in W ) by A1, A2, Def4;
then x is object of (W -SUP_category ) by Def5;
hence x in the carrier of (W -SUP_category ) ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W -SUP_category ) or x in the carrier of (W -INF_category ) )
assume A3: x in the carrier of (W -SUP_category ) ; :: thesis: x in the carrier of (W -INF_category )
then reconsider x = x as LATTICE by YELLOW21:def 4;
( x is strict & x is complete & the carrier of x in W ) by A1, A3, Def5;
then x is object of (W -INF_category ) by Def4;
hence x in the carrier of (W -INF_category ) ; :: thesis: verum