theorem Th51: :: WAYBEL34:51

for W being with_non-empty_element set
for a, b being Object of (W -CL-opp_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )