:: deftheorem Def11 defines idsMap WAYBEL23:def 11 :
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b₃ being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) holds
( b₃ = idsMap S iff for I being Ideal of S ex J being Subset of L st
( I = J & b₃ . I = downarrow J ) );