:: deftheorem Def10 defines sup_func POSET_1:def 10 :
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for b₄ being Function of P,Q holds
( b₄ = sup_func F iff for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₄ . p = sup M );