let W be with_non-empty_element set ; :: thesis: for L being LATTICE st the carrier of L in W holds
( L is Object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) )
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category) by ALTCAT_2:def 11;
A3: the carrier of (W -CL_category) c= the carrier of (W -INF(SC)_category) by ALTCAT_2:def 11;
let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) ) )
assume A4: the carrier of L in W ; :: thesis: ( L is Object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) )
hereby :: thesis: ( L is strict & L is complete & L is continuous implies L is Object of (W -CL_category) )
assume A5: L is Object of (W -CL_category) ; :: thesis: ( L is strict & L is complete & L is continuous )
then L in the carrier of (W -CL_category) ;
then reconsider a = L as Object of (W -INF(SC)_category) by A3;
A6: a in the carrier of (W -INF(SC)_category) ;
latt a is continuous by A5, Def12;
hence ( L is strict & L is complete & L is continuous ) by A1, A2, A6, Def4; :: thesis: verum
end;
assume A7: ( L is strict & L is complete & L is continuous ) ; :: thesis: L is Object of (W -CL_category)
then L is Object of (W -INF_category) by A4, Def4;
then reconsider a = L as Object of (W -INF(SC)_category) by Def10;
latt a = L ;
hence L is Object of (W -CL_category) by A7, Def12; :: thesis: verum