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-opp_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 11;
A2: the carrier of (W -SUP(SO)_category ) c= the carrier of (W -SUP_category ) by ALTCAT_2:def 11;
A3: the carrier of (W -CL-opp_category ) c= the carrier of (W -SUP(SO)_category ) by ALTCAT_2:def 11;
let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is object of (W -CL-opp_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-opp_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-opp_category ) )

assume A5: L is object of (W -CL-opp_category ) ; :: thesis: ( L is strict & L is complete & L is continuous )
then L in the carrier of (W -CL-opp_category ) ;
then reconsider a = L as object of (W -SUP(SO)_category ) by A3;
a in the carrier of (W -SUP(SO)_category ) ;
then ( L is object of (W -SUP_category ) & latt a is continuous ) by A2, A5, Def13;
hence ( L is strict & L is complete & L is continuous ) by A1, Def5; :: thesis: verum

end;

assume A6: ( L is strict & L is complete & L is continuous ) ; :: thesis: L is object of (W -CL-opp_category )
then L is object of (W -SUP_category ) by A4, Def5;
then reconsider a = L as object of (W -SUP(SO)_category ) by Def11;
latt a = L ;
hence L is object of (W -CL-opp_category ) by A6, Def13; :: thesis: verum