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 -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) )

assume A1: the carrier of L in W ; :: thesis: ( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

then reconsider a = L as Object of (W -UPS_category) by A1, Th14;

latt a = L ;

hence L is Object of (W -CONT_category) by A2, Def11; :: thesis: verum

( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

let L be LATTICE; :: thesis: ( the carrier of L in W implies ( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) )

assume A1: the carrier of L in W ; :: thesis: ( L is Object of (W -CONT_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 -CONT_category) )

assume A2:
( L is strict & L is complete & L is continuous )
; :: thesis: L is Object of (W -CONT_category)assume
L is Object of (W -CONT_category)
; :: thesis: ( L is strict & L is complete & L is continuous )

then reconsider a = L as Object of (W -CONT_category) ;

( L = latt a & a is Object of (W -UPS_category) ) by ALTCAT_2:29;

hence ( L is strict & L is complete & L is continuous ) by A1, Def11, Th14; :: thesis: verum

end;then reconsider a = L as Object of (W -CONT_category) ;

( L = latt a & a is Object of (W -UPS_category) ) by ALTCAT_2:29;

hence ( L is strict & L is complete & L is continuous ) by A1, Def11, Th14; :: thesis: verum

then reconsider a = L as Object of (W -UPS_category) by A1, Th14;

latt a = L ;

hence L is Object of (W -CONT_category) by A2, Def11; :: thesis: verum