theorem Th44: :: WAYBEL34:44

for W being with_non-empty_element set
for a, b being Object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )