theorem Th43: :: WAYBEL34:43

for W being with_non-empty_element set
for L being LATTICE holds
( L is Object of (W -INF(SC)_category) iff ( L is strict & L is complete & the carrier of L in W ) )