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 10;
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 object ; :: 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;
A3: ( x is strict & x is complete ) by A1, A2, Def4;
the carrier of x in W by A1, A2, Def4;
then x is Object of (W -SUP_category) by A3, Def5;
hence x in the carrier of (W -SUP_category) ; :: thesis: verum
end;
let x be object ; :: 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 A4: 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;
A5: ( x is strict & x is complete ) by A1, A4, Def5;
the carrier of x in W by A1, A4, Def5;
then x is Object of (W -INF_category) by A5, Def4;
hence x in the carrier of (W -INF_category) ; :: thesis: verum