:: deftheorem defines is_FG_set WAYBEL16:def 2 :
for S being non empty complete continuous Poset
for A being Subset of S holds
( A is_FG_set iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );